Finset

📁 Source: Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_sum_le_sum_abs, abs_sum_of_nonneg, abs_sum_of_nonneg', addLECancellable_sum, add_le_sum, apply_prod_le_sum_apply, apply_sup_le_sum, apply_union_le_sum, card_biUnion_le_card_mul, card_le_card_biUnion, card_le_card_biUnion_add_card_fiber, card_le_card_biUnion_add_one, card_le_mul_card_image, card_le_mul_card_image_of_maps_to, card_nsmul_le_sum, exists_le_of_prod_le', exists_le_of_sum_le, exists_lt_of_prod_lt', exists_lt_of_sum_lt, exists_one_lt_of_prod_one_of_exists_ne_one', exists_pos_of_sum_zero_of_exists_nonzero, le_prod_nonempty_of_submultiplicative, le_prod_nonempty_of_submultiplicative_on_pred, le_prod_of_submultiplicative, le_prod_of_submultiplicative_on_pred, le_sum_card, le_sum_card_inter, le_sum_nonempty_of_subadditive, le_sum_nonempty_of_subadditive_on_pred, le_sum_of_subadditive, le_sum_of_subadditive_on_pred, max_prod_le, max_sum_le, mulLECancellable_prod, mul_card_image_le_card, mul_card_image_le_card_of_maps_to, mul_le_prod, one_le_prod', one_le_prod'', one_lt_prod, one_lt_prod', one_lt_prod_iff, one_lt_prod_iff_of_one_le, pow_card_le_prod, prod_anti_set_of_le_one', prod_eq_one_iff_of_le_one', prod_eq_one_iff_of_one_le', prod_eq_prod_iff_of_le, prod_fiberwise_le_prod_of_one_le_prod_fiber', prod_image_le_of_one_le, prod_le_one', prod_le_pow_card, prod_le_prod', prod_le_prod_fiberwise_of_prod_fiber_le_one', prod_le_prod_of_ne_one', prod_le_prod_of_subset', prod_le_prod_of_subset_of_le_one', prod_le_prod_of_subset_of_one_le', prod_le_univ_prod_of_one_le', prod_lt_one, prod_lt_one', prod_lt_one_iff_of_le_one, prod_lt_prod', prod_lt_prod_of_nonempty', prod_lt_prod_of_subset', prod_min_le, prod_mono_set', prod_mono_set_of_one_le', prod_sdiff_le_prod_sdiff, prod_sdiff_lt_prod_sdiff, single_le_prod', single_le_prod_of_canonicallyOrdered, single_le_sum, single_le_sum_of_canonicallyOrdered, single_lt_prod', single_lt_sum, sum_anti_set_of_nonpos', sum_apply_le_apply_prod, sum_card, sum_card_inter, sum_card_inter_le, sum_card_le, sum_eq_sum_iff_of_le, sum_eq_zero_iff_of_nonneg, sum_eq_zero_iff_of_nonpos, sum_fiberwise_le_sum_of_sum_fiber_nonneg, sum_image_le_of_nonneg, sum_le_card_nsmul, sum_le_one_iff, sum_le_sum, sum_le_sum_fiberwise_of_sum_fiber_nonpos, sum_le_sum_of_ne_zero, sum_le_sum_of_subset, sum_le_sum_of_subset_of_nonneg, sum_le_sum_of_subset_of_nonpos', sum_le_univ_sum_of_nonneg, sum_lt_sum, sum_lt_sum_of_nonempty, sum_lt_sum_of_subset, sum_min_le, sum_mono_set, sum_mono_set_of_nonneg, sum_neg, sum_neg', sum_neg_iff_of_nonpos, sum_nonneg, sum_nonneg', sum_nonpos, sum_pos, sum_pos', sum_pos_iff, sum_pos_iff_of_nonneg, sum_sdiff_le_sum_sdiff, sum_sdiff_lt_sum_sdiff, one_le_prod, one_lt_prod, one_lt_prod_iff_of_one_le, prod_eq_one_iff_of_le_one, prod_eq_one_iff_of_one_le, prod_le_one, prod_lt_one, prod_lt_one_iff_of_le_one, prod_mono', prod_strictMono', sum_eq_zero_iff_of_nonneg, sum_eq_zero_iff_of_nonpos, sum_mono, sum_neg, sum_neg_iff_of_nonpos, sum_nonneg, sum_nonpos, sum_pos, sum_pos_iff_of_nonneg, sum_strictMono, card_le_card_toFinset_add_one_iff, finset_sum_eq_sup_iff_disjoint, sup_powerset_len	137
Total	137

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_sum_le_sum_abs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup sum AddCommGroup.toAddCommMonoid	—	le_sum_of_subadditive Eq.le abs_zero IsOrderedAddMonoid.toAddLeftMono abs_add_le
abs_sum_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup sum AddCommGroup.toAddCommMonoid	—	abs_of_nonneg sum_nonneg
abs_sum_of_nonneg' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup sum AddCommGroup.toAddCommMonoid	—	abs_of_nonneg sum_nonneg'
addLECancellable_sum 📖	mathematical	—	AddLECancellable AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	cons_induction addLECancellable_zero notMem_empty IsEmpty.forall_iff instIsEmptyFalse sum_cons addLECancellable_add mem_cons
add_le_sum 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike	Preorder.toLE AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	mem_singleton sum_cons sum_singleton sum_le_sum_of_subset_of_nonneg cons_subset singleton_subset_iff
apply_prod_le_sum_apply 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulOne.toMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	Preorder.toLE prod sum	—	LE.le.trans_eq Multiset.apply_prod_le_sum_map Multiset.map_map sum_map_val
apply_sup_le_sum 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SemilatticeSup.toMax AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	Preorder.toLE sup sum	—	induction_on Eq.le sup_insert sum_insert LE.le.trans add_le_add_right
apply_union_le_sum 📖	mathematical	Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE Set.instUnion AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	Preorder.toLE Set.iUnion Finset SetLike.instMembership instSetLike sum	—	apply_sup_le_sum sup_set_eq_biUnion
card_biUnion_le_card_mul 📖	mathematical	card	card biUnion	—	LE.le.trans card_biUnion_le sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
card_le_card_biUnion 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot SetLike.coe instSetLike Nonempty	card biUnion	—	card_biUnion card_eq_sum_ones sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nonempty.card_pos
card_le_card_biUnion_add_card_fiber 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot SetLike.coe instSetLike	card biUnion filter Finset instEmptyCollection decidableEq	—	card_filter_add_card_filter_not add_comm le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid card_le_card_biUnion Set.PairwiseDisjoint.subset filter_subset nonempty_of_ne_empty mem_filter le_refl card_le_card biUnion_subset_biUnion_of_subset_left
card_le_card_biUnion_add_one 📖	mathematical	Finset Set.PairwiseDisjoint partialOrder instOrderBot SetLike.coe instSetLike	card biUnion	—	le_imp_le_of_le_of_le card_le_card_biUnion_add_card_fiber le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid card_le_one mem_filter
card_le_mul_card_image 📖	mathematical	card filter	card image	—	card_le_mul_card_image_of_maps_to mem_image_of_mem
card_le_mul_card_image_of_maps_to 📖	mathematical	Finset SetLike.instMembership instSetLike card filter	card	—	card_eq_sum_card_fiberwise sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid sum_const mul_comm
card_nsmul_le_sum 📖	mathematical	Preorder.toLE	Preorder.toLE AddMonoid.toNSMul AddCommMonoid.toAddMonoid card sum	—	sum_le_card_nsmul OrderDual.addLeftMono
exists_le_of_prod_le' 📖	mathematical	Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder prod	Finset SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq prod_lt_prod_of_nonempty' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid
exists_le_of_sum_le 📖	mathematical	Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder sum	Finset SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq not_le sum_lt_sum_of_nonempty IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
exists_lt_of_prod_lt' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder prod	Finset SetLike.instMembership instSetLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq prod_le_prod'
exists_lt_of_sum_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder sum	Finset SetLike.instMembership instSetLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq not_lt sum_le_sum
exists_one_lt_of_prod_one_of_exists_ne_one' 📖	mathematical	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike	Finset SetLike.instMembership instSetLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq ne_of_lt prod_lt_prod' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid LE.le.lt_of_ne prod_const_one
exists_pos_of_sum_zero_of_exists_nonzero 📖	mathematical	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike	Finset SetLike.instMembership instSetLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq not_lt ne_of_lt sum_lt_sum IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid LE.le.lt_of_ne sum_const_zero
le_prod_nonempty_of_submultiplicative 📖	mathematical	Preorder.toLE MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Nonempty	Preorder.toLE prod	—	le_prod_nonempty_of_submultiplicative_on_pred
le_prod_nonempty_of_submultiplicative_on_pred 📖	mathematical	Preorder.toLE MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Nonempty	Preorder.toLE prod	—	le_trans Multiset.le_prod_nonempty_of_submultiplicative_on_pred Nonempty.ne_empty Multiset.forall_mem_map_iff Multiset.map_map Multiset.map_congr instReflLe
le_prod_of_submultiplicative 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toMul	Preorder.toLE prod	—	le_trans Multiset.le_prod_of_submultiplicative Multiset.map_map Multiset.map_congr instReflLe
le_prod_of_submultiplicative_on_pred 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toMul	Preorder.toLE prod	—	eq_empty_or_nonempty le_prod_nonempty_of_submultiplicative_on_pred
le_sum_card 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	Fintype.card sum Finset Nat.instAddCommMonoid card	—	le_sum_card_inter sum_congr univ_inter
le_sum_card_inter 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	card sum Finset Nat.instAddCommMonoid instInter	—	LE.le.trans card_nsmul_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid sum_congr card_eq_sum_ones sum_filter Eq.le sum_comm
le_sum_nonempty_of_subadditive 📖	mathematical	Preorder.toLE AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nonempty	Preorder.toLE sum	—	le_sum_nonempty_of_subadditive_on_pred
le_sum_nonempty_of_subadditive_on_pred 📖	mathematical	Preorder.toLE AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nonempty	Preorder.toLE sum	—	le_trans Multiset.le_sum_nonempty_of_subadditive_on_pred Multiset.map_eq_zero val_eq_zero Nonempty.ne_empty Multiset.forall_mem_map_iff Multiset.map_map Multiset.map_congr instReflLe
le_sum_of_subadditive 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd	Preorder.toLE sum	—	le_trans Multiset.le_sum_of_subadditive Multiset.map_map Multiset.map_congr instReflLe
le_sum_of_subadditive_on_pred 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd	Preorder.toLE sum	—	eq_empty_or_nonempty le_sum_nonempty_of_subadditive_on_pred
max_prod_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup prod	—	Multiset.max_prod_le
max_sum_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup sum	—	Multiset.max_sum_le
mulLECancellable_prod 📖	mathematical	—	MulLECancellable MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	cons_induction instIsEmptyFalse prod_cons
mul_card_image_le_card 📖	mathematical	card filter	card image	—	mul_card_image_le_card_of_maps_to mem_image_of_mem
mul_card_image_le_card_of_maps_to 📖	mathematical	Finset SetLike.instMembership instSetLike card filter	card	—	sum_const mul_comm sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid card_eq_sum_card_fiberwise
mul_le_prod 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike	Preorder.toLE MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	prod_cons prod_singleton prod_le_prod_of_subset_of_one_le'
one_le_prod' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	le_trans prod_const_one le_refl prod_le_prod'
one_le_prod'' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	one_le_prod'
one_lt_prod 📖	mathematical	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Nonempty	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	lt_of_le_of_lt prod_const_one le_refl prod_lt_prod_of_nonempty'
one_lt_prod' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod	—	Eq.trans_lt prod_const_one prod_lt_prod'
one_lt_prod_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Finset SetLike.instMembership instSetLike	—	CanonicallyOrderedMul.toIsOrderedMonoid one_lt_prod_iff_of_one_le IsOrderedMonoid.toMulLeftMono one_le
one_lt_prod_iff_of_one_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Finset SetLike.instMembership instSetLike	—	one_le_prod' LE.le.lt_iff_ne' prod_eq_one_iff_of_one_le'
pow_card_le_prod 📖	mathematical	Preorder.toLE	Preorder.toLE Monoid.toPow CommMonoid.toMonoid card prod	—	prod_le_pow_card OrderDual.mulLeftMono
prod_anti_set_of_le_one' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Antitone Finset PartialOrder.toPreorder partialOrder prod	—	prod_le_prod_of_subset_of_le_one'
prod_eq_one_iff_of_le_one' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_eq_one_iff_of_one_le' OrderDual.mulLeftMono
prod_eq_one_iff_of_one_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	induction_on notMem_empty mem_insert_of_mem prod_insert mul_eq_one_iff_of_one_le covariant_swap_mul_of_covariant_mul mem_insert_self one_le_prod' forall_mem_insert
prod_eq_prod_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	prod	—	induction_on notMem_empty prod_insert forall_mem_insert mem_insert_of_mem mul_eq_mul_iff_eq_and_eq IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT IsOrderedCancelMonoid.toMulLeftReflectLT covariant_swap_mul_of_covariant_mul mem_insert_self prod_le_prod'
prod_fiberwise_le_prod_of_one_le_prod_fiber' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod filter	Preorder.toLE prod filter	—	prod_le_prod_of_subset_of_one_le' subset_union_left prod_fiberwise_of_maps_to mem_union mem_image_of_mem
prod_image_le_of_one_le 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod image	—	prod_comp prod_le_prod' mem_image le_self_pow card_pos mem_filter
prod_le_one' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	LE.le.trans_eq prod_le_prod' prod_const_one
prod_le_pow_card 📖	mathematical	Preorder.toLE	Preorder.toLE prod Monoid.toPow CommMonoid.toMonoid card	—	LE.le.trans Multiset.prod_le_pow_card Multiset.card_map instReflLe
prod_le_prod' 📖	mathematical	Preorder.toLE	Preorder.toLE prod	—	Multiset.prod_map_le_prod_map
prod_le_prod_fiberwise_of_prod_fiber_le_one' 📖	mathematical	Preorder.toLE prod filter MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod filter	—	prod_fiberwise_le_prod_of_one_le_prod_fiber' OrderDual.mulLeftMono
prod_le_prod_of_ne_one' 📖	mathematical	Finset SetLike.instMembership instSetLike	Preorder.toLE prod	—	CanonicallyOrderedMul.toIsOrderedMonoid prod_union disjoint_filter filter_union_filter_not_eq mul_le_of_le_one_of_le covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono prod_le_one' le_of_eq prod_le_prod_of_subset'
prod_le_prod_of_subset' 📖	mathematical	Finset instHasSubset	Preorder.toLE prod	—	CanonicallyOrderedMul.toIsOrderedMonoid prod_le_prod_of_subset_of_one_le' IsOrderedMonoid.toMulLeftMono one_le
prod_le_prod_of_subset_of_le_one' 📖	mathematical	Finset instHasSubset Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod	—	prod_le_prod_of_subset_of_one_le' OrderDual.mulLeftMono
prod_le_prod_of_subset_of_one_le' 📖	mathematical	Finset instHasSubset Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod	—	le_mul_of_one_le_left' covariant_swap_mul_of_covariant_mul one_le_prod' prod_union sdiff_disjoint sdiff_union_of_subset
prod_le_univ_prod_of_one_le' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE prod univ	—	prod_le_prod_of_subset_of_one_le' subset_univ
prod_lt_one 📖	mathematical	Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Nonempty	Preorder.toLT prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	LT.lt.trans_le prod_lt_prod_of_nonempty' prod_const_one le_refl
prod_lt_one' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	LE.le.trans_lt' Eq.le prod_const_one prod_lt_prod'
prod_lt_one_iff_of_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike	—	one_lt_prod_iff_of_one_le OrderDual.mulLeftMono
prod_lt_prod' 📖	mathematical	Preorder.toLE Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT prod	—	Multiset.prod_lt_prod'
prod_lt_prod_of_nonempty' 📖	mathematical	Nonempty Preorder.toLT	Preorder.toLT prod	—	Multiset.prod_lt_prod_of_nonempty'
prod_lt_prod_of_subset' 📖	mathematical	Finset instHasSubset SetLike.instMembership instSetLike Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLE	Preorder.toLT prod	—	prod_insert lt_mul_of_one_lt_left' covariant_swap_mul_of_covariant_mul prod_le_prod_of_subset_of_one_le' IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid
prod_min_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder prod SemilatticeInf.toMin	—	Multiset.prod_min_le
prod_mono_set' 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder prod	—	CanonicallyOrderedMul.toIsOrderedMonoid prod_le_prod_of_subset'
prod_mono_set_of_one_le' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Monotone Finset PartialOrder.toPreorder partialOrder prod	—	prod_le_prod_of_subset_of_one_le'
prod_sdiff_le_prod_sdiff 📖	mathematical	—	Preorder.toLE prod Finset instSDiff	—	mul_le_mul_iff_right covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid contravariant_swap_mul_of_contravariant_mul IsOrderedCancelMonoid.toMulLeftReflectLE prod_union disjoint_sdiff_inter sdiff_union_inter inter_comm
prod_sdiff_lt_prod_sdiff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder prod Finset instSDiff	—	mul_lt_mul_iff_right IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLT covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid prod_union disjoint_sdiff_inter sdiff_union_inter inter_comm
single_le_prod' 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike	Preorder.toLE prod	—	prod_singleton prod_le_prod_of_subset_of_one_le' singleton_subset_iff
single_le_prod_of_canonicallyOrdered 📖	mathematical	Finset SetLike.instMembership instSetLike	Preorder.toLE prod	—	CanonicallyOrderedMul.toIsOrderedMonoid single_le_prod' IsOrderedMonoid.toMulLeftMono one_le
single_le_sum 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike	Preorder.toLE sum	—	sum_singleton sum_le_sum_of_subset_of_nonneg singleton_subset_iff
single_le_sum_of_canonicallyOrdered 📖	mathematical	Finset SetLike.instMembership instSetLike	Preorder.toLE sum	—	CanonicallyOrderedAdd.toIsOrderedAddMonoid single_le_sum IsOrderedAddMonoid.toAddLeftMono zero_le
single_lt_prod' 📖	mathematical	Finset SetLike.instMembership instSetLike Preorder.toLT MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLE	Preorder.toLT prod	—	prod_singleton prod_lt_prod_of_subset' singleton_subset_iff mem_singleton
single_lt_sum 📖	mathematical	Finset SetLike.instMembership instSetLike Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE	Preorder.toLT sum	—	sum_singleton sum_lt_sum_of_subset singleton_subset_iff mem_singleton
sum_anti_set_of_nonpos' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Antitone Finset PartialOrder.toPreorder partialOrder sum	—	sum_le_sum_of_subset_of_nonpos'
sum_apply_le_apply_prod 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MulOne.toMul	Preorder.toLE sum prod	—	apply_prod_le_sum_apply OrderDual.addLeftMono
sum_card 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	sum Finset Nat.instAddCommMonoid card Fintype.card	—	sum_card_inter sum_congr univ_inter
sum_card_inter 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	sum Finset Nat.instAddCommMonoid card instInter	—	LE.le.antisymm sum_card_inter_le Eq.le le_sum_card_inter Eq.ge
sum_card_inter_le 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	sum Finset Nat.instAddCommMonoid card instInter	—	le_trans sum_congr card_eq_sum_ones sum_filter Eq.le sum_comm sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
sum_card_le 📖	mathematical	card Finset filter SetLike.instMembership instSetLike decidableMem	sum Finset Nat.instAddCommMonoid card Fintype.card	—	sum_congr univ_inter sum_card_inter_le
sum_eq_sum_iff_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	sum	—	induction_on notMem_empty sum_insert forall_mem_insert mem_insert_of_mem add_eq_add_iff_eq_and_eq IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add mem_insert_self sum_le_sum
sum_eq_zero_iff_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	induction_on notMem_empty mem_insert_of_mem sum_insert add_eq_zero_iff_of_nonneg covariant_swap_add_of_covariant_add mem_insert_self sum_nonneg forall_mem_insert
sum_eq_zero_iff_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_eq_zero_iff_of_nonneg OrderDual.addLeftMono
sum_fiberwise_le_sum_of_sum_fiber_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum filter	Preorder.toLE sum filter	—	sum_le_sum_of_subset_of_nonneg subset_union_left sum_fiberwise_of_maps_to mem_union mem_image_of_mem
sum_image_le_of_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum image	—	sum_comp sum_le_sum mem_image le_self_nsmul card_pos mem_filter
sum_le_card_nsmul 📖	mathematical	Preorder.toLE	Preorder.toLE sum AddMonoid.toNSMul AddCommMonoid.toAddMonoid card	—	LE.le.trans Multiset.sum_le_card_nsmul Multiset.mem_map Multiset.card_map instReflLe
sum_le_one_iff 📖	mathematical	—	sum Nat.instAddCommMonoid	—	LE.le.trans sum_mono_set Nat.instCanonicallyOrderedAdd sum_sdiff singleton_subset_iff sum_congr sum_const_zero sum_singleton zero_add instReflLe Mathlib.Tactic.Push.not_and_eq
sum_le_sum 📖	mathematical	Preorder.toLE	Preorder.toLE sum	—	Multiset.sum_map_le_sum_map
sum_le_sum_fiberwise_of_sum_fiber_nonpos 📖	mathematical	Preorder.toLE sum filter AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum filter	—	sum_fiberwise_le_sum_of_sum_fiber_nonneg OrderDual.addLeftMono
sum_le_sum_of_ne_zero 📖	mathematical	Finset SetLike.instMembership instSetLike	Preorder.toLE sum	—	CanonicallyOrderedAdd.toIsOrderedAddMonoid sum_union disjoint_filter filter_union_filter_not_eq add_le_of_nonpos_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sum_nonpos mem_filter le_of_eq sum_le_sum_of_subset subset_iff
sum_le_sum_of_subset 📖	mathematical	Finset instHasSubset	Preorder.toLE sum	—	CanonicallyOrderedAdd.toIsOrderedAddMonoid sum_le_sum_of_subset_of_nonneg IsOrderedAddMonoid.toAddLeftMono zero_le
sum_le_sum_of_subset_of_nonneg 📖	mathematical	Finset instHasSubset Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum	—	le_add_of_nonneg_left covariant_swap_add_of_covariant_add sum_nonneg mem_sdiff sum_union sdiff_disjoint sdiff_union_of_subset
sum_le_sum_of_subset_of_nonpos' 📖	mathematical	Finset instHasSubset Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum	—	sum_le_sum_of_subset_of_nonneg OrderDual.addLeftMono
sum_le_univ_sum_of_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum univ	—	sum_le_sum_of_subset_of_nonneg subset_univ
sum_lt_sum 📖	mathematical	Preorder.toLE Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT sum	—	Multiset.sum_lt_sum
sum_lt_sum_of_nonempty 📖	mathematical	Nonempty Preorder.toLT	Preorder.toLT sum	—	Multiset.sum_lt_sum_of_nonempty val_eq_zero not_nonempty_empty
sum_lt_sum_of_subset 📖	mathematical	Finset instHasSubset SetLike.instMembership instSetLike Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE	Preorder.toLT sum	—	sum_insert lt_add_of_pos_left covariant_swap_add_of_covariant_add sum_le_sum_of_subset_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid insert_subset_iff mem_insert
sum_min_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder sum SemilatticeInf.toMin	—	Multiset.sum_min_le
sum_mono_set 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder sum	—	CanonicallyOrderedAdd.toIsOrderedAddMonoid sum_le_sum_of_subset
sum_mono_set_of_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Monotone Finset PartialOrder.toPreorder partialOrder sum	—	sum_le_sum_of_subset_of_nonneg
sum_neg 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nonempty	Preorder.toLT sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LT.lt.trans_le sum_lt_sum_of_nonempty sum_const_zero le_refl
sum_neg' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LE.le.trans_lt' Eq.le sum_const_zero sum_lt_sum
sum_neg_iff_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike	—	sum_pos_iff_of_nonneg OrderDual.addLeftMono
sum_nonneg 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	le_trans sum_const_zero le_refl sum_le_sum
sum_nonneg' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	sum_nonneg
sum_nonpos 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LE.le.trans_eq sum_le_sum sum_const_zero
sum_pos 📖	mathematical	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nonempty	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	lt_of_le_of_lt sum_const_zero le_refl sum_lt_sum_of_nonempty
sum_pos' 📖	mathematical	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike Preorder.toLT	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum	—	Eq.trans_lt sum_const_zero sum_lt_sum
sum_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Finset SetLike.instMembership instSetLike	—	CanonicallyOrderedAdd.toIsOrderedAddMonoid sum_pos_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono zero_le
sum_pos_iff_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Finset SetLike.instMembership instSetLike	—	sum_nonneg LE.le.lt_iff_ne' sum_eq_zero_iff_of_nonneg
sum_sdiff_le_sum_sdiff 📖	mathematical	—	Preorder.toLE sum Finset instSDiff	—	add_le_add_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLE sum_union disjoint_sdiff_inter sdiff_union_inter inter_comm
sum_sdiff_lt_sum_sdiff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder sum Finset instSDiff	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid sum_union disjoint_sdiff_inter sdiff_union_inter inter_comm

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_le_prod 📖	mathematical	Pi.hasLe Preorder.toLE Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod Finset.univ	—	Finset.one_le_prod'
one_lt_prod 📖	mathematical	Preorder.toLT Pi.preorder PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod Finset.univ	—	Finset.one_lt_prod' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid LT.lt.le Pi.lt_def
one_lt_prod_iff_of_one_le 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod Finset.univ Pi.preorder Pi.instOne	—	LE.le.eq_or_lt Finset.prod_congr Finset.prod_const_one
prod_eq_one_iff_of_le_one 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Pi.instOne	—	Finset.prod_eq_one_iff_of_le_one'
prod_eq_one_iff_of_one_le 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Pi.instOne	—	Finset.prod_eq_one_iff_of_one_le'
prod_le_one 📖	mathematical	Pi.hasLe Preorder.toLE Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLE Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_le_one'
prod_lt_one 📖	mathematical	Preorder.toLT Pi.preorder PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_lt_one' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid LT.lt.le Pi.lt_def
prod_lt_one_iff_of_le_one 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instOne MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Pi.preorder Pi.instOne	—	LE.le.eq_or_lt Finset.prod_congr Finset.prod_const_one
prod_mono' 📖	mathematical	—	Monotone Pi.preorder Finset.prod Finset.univ	—	Finset.prod_le_prod'
prod_strictMono' 📖	mathematical	—	StrictMono Pi.preorder PartialOrder.toPreorder Finset.prod Finset.univ	—	Pi.lt_def Finset.prod_lt_prod' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid Finset.mem_univ
sum_eq_zero_iff_of_nonneg 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.instZero	—	Finset.sum_eq_zero_iff_of_nonneg Finset.mem_univ
sum_eq_zero_iff_of_nonpos 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.instZero	—	Finset.sum_eq_zero_iff_of_nonpos Finset.mem_univ
sum_mono 📖	mathematical	—	Monotone Pi.preorder Finset.sum Finset.univ	—	Finset.sum_le_sum
sum_neg 📖	mathematical	Preorder.toLT Pi.preorder PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_neg' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid LT.lt.le Finset.mem_univ Pi.lt_def
sum_neg_iff_of_nonpos 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.preorder Pi.instZero	—	LE.le.eq_or_lt Finset.sum_congr Finset.sum_const_zero lt_self_iff_false sum_neg
sum_nonneg 📖	mathematical	Pi.hasLe Preorder.toLE Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum Finset.univ	—	Finset.sum_nonneg
sum_nonpos 📖	mathematical	Pi.hasLe Preorder.toLE Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLE Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_nonpos
sum_pos 📖	mathematical	Preorder.toLT Pi.preorder PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum Finset.univ	—	Finset.sum_pos' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid LT.lt.le Finset.mem_univ Pi.lt_def
sum_pos_iff_of_nonneg 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum Finset.univ Pi.preorder Pi.instZero	—	LE.le.eq_or_lt Finset.sum_congr Finset.sum_const_zero lt_self_iff_false sum_pos
sum_strictMono 📖	mathematical	—	StrictMono Pi.preorder PartialOrder.toPreorder Finset.sum Finset.univ	—	Pi.lt_def Finset.sum_lt_sum IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid Finset.mem_univ

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le_card_toFinset_add_one_iff 📖	mathematical	—	card Finset.card toFinset count	—	toFinset_sum_count_eq Finset.card_eq_sum_ones tsub_le_iff_left Nat.instOrderedSub Finset.sum_tsub_distrib IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Finset.sum_le_one_iff one_le_count_iff_mem LT.lt.le
finset_sum_eq_sup_iff_disjoint 📖	mathematical	—	Finset.sum Multiset AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid Finset.sup Lattice.toSemilatticeSup instLattice instOrderBot Disjoint instPartialOrder	—	Finset.cons_induction_on Finset.sup_empty instIsEmptyFalse Finset.sum_cons Finset.sup_cons add_eq_union_left_of_le Finset.sup_le le_sum_of_mem mem_map_of_mem instCanonicallyOrderedAdd
sup_powerset_len 📖	mathematical	—	Finset.sup Multiset Lattice.toSemilatticeSup instLattice decidableEq instOrderBot Finset.range card powersetCard powerset	—	bind.eq_1 join.eq_1 Finset.range_val Finset.sum_eq_multiset_sum finset_sum_eq_sup_iff_disjoint pairwise_disjoint_powersetCard bind_powerset_len

---

← Back to Index