Finset

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

Statistics

Metric	Count
Definitions	0
Theorems `single_le_sum`, `single_le_prod`, `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`	139
Total	139

CanonicallyOrderedAddCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_le_sum` 📖	mathematical	`Finset` `Finset.instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `Finset.sum`	—	`Finset.single_le_sum_of_canonicallyOrdered`

CanonicallyOrderedCommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_le_prod` 📖	mathematical	`Finset` `Finset.instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `Finset.prod`	—	`Finset.single_le_prod_of_canonicallyOrdered`

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` `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` `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` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership`	`AddZero.toAdd` `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`	`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`	`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` `PartialOrder.toPreorder` `Set.instUnion` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Set.iUnion` `Finset` `instMembership` `sum`	—	`apply_sup_le_sum` `sup_set_eq_biUnion`
`card_biUnion_le_card_mul` 📖	mathematical	`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` `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`	`image`	—	`card_le_mul_card_image_of_maps_to` `mem_image_of_mem`
`card_le_mul_card_image_of_maps_to` 📖	—	`Finset` `instMembership` `card` `filter`	—	—	`card_eq_sum_card_fiberwise` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `sum_const` `mul_comm`
`card_nsmul_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddMonoid.toNatSMul` `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` `instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `prod_lt_prod_of_nonempty'`
`exists_le_of_sum_le` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum`	`Finset` `instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `not_le` `sum_lt_sum_of_nonempty`
`exists_lt_of_prod_lt'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `prod`	`Finset` `instMembership`	—	`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` `instMembership`	—	`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` `instMembership`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `ne_of_lt` `prod_lt_prod'` `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` `instMembership`	`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` `ne_of_lt` `sum_lt_sum` `LE.le.lt_of_ne` `sum_const_zero`
`le_prod_nonempty_of_submultiplicative` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Nonempty`	`prod`	—	`le_prod_nonempty_of_submultiplicative_on_pred`
`le_prod_nonempty_of_submultiplicative_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Nonempty`	`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`
`le_prod_of_submultiplicative` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	`prod`	—	`le_trans` `Multiset.le_prod_of_submultiplicative` `Multiset.map_map` `Multiset.map_congr`
`le_prod_of_submultiplicative_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	`prod`	—	`eq_empty_or_nonempty` `le_prod_nonempty_of_submultiplicative_on_pred`
`le_sum_card` 📖	mathematical	`card` `Finset` `filter` `instMembership` `decidableMem`	`Fintype.card` `sum` `Nat.instAddCommMonoid`	—	`le_sum_card_inter` `sum_congr` `univ_inter`
`le_sum_card_inter` 📖	mathematical	`card` `Finset` `filter` `instMembership` `decidableMem`	`sum` `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` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty`	`sum`	—	`le_sum_nonempty_of_subadditive_on_pred`
`le_sum_nonempty_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty`	`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` `le_refl`
`le_sum_of_subadditive` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	`sum`	—	`le_trans` `Multiset.le_sum_of_subadditive` `Multiset.map_map` `Multiset.map_congr` `le_refl`
`le_sum_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	`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`	`image`	—	`mul_card_image_le_card_of_maps_to` `mem_image_of_mem`
`mul_card_image_le_card_of_maps_to` 📖	—	`Finset` `instMembership` `card` `filter`	—	—	`sum_const` `mul_comm` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `card_eq_sum_card_fiberwise`
`mul_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset` `instMembership`	`MulOne.toMul` `prod`	—	`prod_cons` `prod_singleton` `prod_le_prod_of_subset_of_one_le'`
`one_le_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`one_le_prod'`
`one_lt_prod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Nonempty`	`prod`	—	`lt_of_le_of_lt` `prod_const_one` `le_refl` `prod_lt_prod_of_nonempty'`
`one_lt_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset` `instMembership` `Preorder.toLT`	`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` `instMembership`	—	`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` `prod` `Finset` `instMembership`	—	`one_le_prod'` `LE.le.lt_iff_ne'` `prod_eq_one_iff_of_one_le'`
`pow_card_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Monoid.toNatPow` `CommMonoid.toMonoid` `card` `prod`	—	`prod_le_pow_card` `OrderDual.mulLeftMono`
`prod_anti_set_of_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Antitone` `Finset` `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`	—	`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`	—	`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` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `mem_insert_self` `prod_le_prod'`
`prod_fiberwise_le_prod_of_one_le_prod_fiber'` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `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` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `image`	—	`prod_comp` `prod_le_prod'` `mem_image` `le_self_pow` `card_pos` `mem_filter`
`prod_le_one'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`LE.le.trans_eq` `prod_le_prod'` `prod_const_one`
`prod_le_pow_card` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod` `Monoid.toNatPow` `CommMonoid.toMonoid` `card`	—	`LE.le.trans` `Multiset.prod_le_pow_card` `Multiset.card_map`
`prod_le_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod`	—	`Multiset.prod_map_le_prod_map`
`prod_le_prod_fiberwise_of_prod_fiber_le_one'` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `prod` `filter` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—	`prod_fiberwise_le_prod_of_one_le_prod_fiber'` `OrderDual.mulLeftMono`
`prod_le_prod_of_ne_one'` 📖	mathematical	`Finset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`prod_le_prod_of_subset_of_one_le'` `OrderDual.mulLeftMono`
`prod_le_prod_of_subset_of_one_le'` 📖	mathematical	`Finset` `instHasSubset` `Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`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` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `univ`	—	`prod_le_prod_of_subset_of_one_le'` `subset_univ`
`prod_lt_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Nonempty`	`prod`	—	`LT.lt.trans_le` `prod_lt_prod_of_nonempty'` `prod_const_one` `le_refl`
`prod_lt_one'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset` `instMembership` `Preorder.toLT`	`prod`	—	`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` `prod` `Finset` `instMembership`	—	`one_lt_prod_iff_of_one_le` `OrderDual.mulLeftMono`
`prod_lt_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Finset` `instMembership` `Preorder.toLT`	`prod`	—	`Multiset.prod_lt_prod'`
`prod_lt_prod_of_nonempty'` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder`	`prod`	—	`Multiset.prod_lt_prod_of_nonempty'`
`prod_lt_prod_of_subset'` 📖	mathematical	`Finset` `instHasSubset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE`	`prod`	—	`prod_insert` `lt_mul_of_one_lt_left'` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `prod_le_prod_of_subset_of_one_le'`
`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` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Monotone` `Finset` `partialOrder` `prod`	—	`prod_le_prod_of_subset_of_one_le'`
`prod_sdiff_le_prod_sdiff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `prod` `Finset` `instSDiff`	—	`mul_le_mul_iff_right` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `IsCancelMul.toIsRightCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `contravariant_swap_mul_of_contravariant_mul` `IsOrderedCancelMonoid.toMulLeftReflectLT` `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` `IsCancelMul.toIsRightCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `contravariant_swap_mul_of_contravariant_mul` `IsOrderedCancelMonoid.toMulLeftReflectLT` `prod_union` `disjoint_sdiff_inter` `sdiff_union_inter` `inter_comm`
`single_le_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset` `instMembership`	`prod`	—	`prod_singleton` `prod_le_prod_of_subset_of_one_le'` `singleton_subset_iff`
`single_le_prod_of_canonicallyOrdered` 📖	mathematical	`Finset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `prod`	—	`CanonicallyOrderedMul.toIsOrderedMonoid` `single_le_prod'` `IsOrderedMonoid.toMulLeftMono` `one_le`
`single_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership`	`sum`	—	`sum_singleton` `sum_le_sum_of_subset_of_nonneg` `singleton_subset_iff`
`single_le_sum_of_canonicallyOrdered` 📖	mathematical	`Finset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `sum`	—	`CanonicallyOrderedAdd.toIsOrderedAddMonoid` `single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `zero_le`
`single_lt_prod'` 📖	mathematical	`Finset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE`	`prod`	—	`prod_singleton` `prod_lt_prod_of_subset'` `singleton_subset_iff` `mem_singleton`
`single_lt_sum` 📖	mathematical	`Finset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE`	`sum`	—	`sum_singleton` `sum_lt_sum_of_subset` `singleton_subset_iff` `mem_singleton`
`sum_anti_set_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Antitone` `Finset` `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`	`sum` `prod`	—	`apply_prod_le_sum_apply` `OrderDual.addLeftMono`
`sum_card` 📖	mathematical	`card` `Finset` `filter` `instMembership` `decidableMem`	`sum` `Nat.instAddCommMonoid` `Fintype.card`	—	`sum_card_inter` `sum_congr` `univ_inter`
`sum_card_inter` 📖	mathematical	`card` `Finset` `filter` `instMembership` `decidableMem`	`sum` `Nat.instAddCommMonoid` `instInter`	—	`LE.le.antisymm` `sum_card_inter_le` `Eq.le` `le_sum_card_inter` `Eq.ge`
`sum_card_inter_le` 📖	mathematical	`card` `Finset` `filter` `instMembership` `decidableMem`	`sum` `Nat.instAddCommMonoid` `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` `instMembership` `decidableMem`	`sum` `Nat.instAddCommMonoid` `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` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `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`	—	`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`	—	`sum_eq_zero_iff_of_nonneg` `OrderDual.addLeftMono`
`sum_fiberwise_le_sum_of_sum_fiber_nonneg` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `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` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `image`	—	`sum_comp` `sum_le_sum` `mem_image` `le_self_nsmul` `card_pos` `mem_filter`
`sum_le_card_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	—	`LE.le.trans` `Multiset.sum_le_card_nsmul` `Multiset.mem_map` `Multiset.card_map` `le_refl`
`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` `Mathlib.Tactic.Push.not_and_eq`
`sum_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum`	—	`Multiset.sum_map_le_sum_map`
`sum_le_sum_fiberwise_of_sum_fiber_nonpos` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `sum` `filter` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`sum_fiberwise_le_sum_of_sum_fiber_nonneg` `OrderDual.addLeftMono`
`sum_le_sum_of_ne_zero` 📖	mathematical	`Finset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `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` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`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` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`sum_le_sum_of_subset_of_nonneg` `OrderDual.addLeftMono`
`sum_le_univ_sum_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `univ`	—	`sum_le_sum_of_subset_of_nonneg` `subset_univ`
`sum_lt_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Finset` `instMembership` `Preorder.toLT`	`sum`	—	`Multiset.sum_lt_sum`
`sum_lt_sum_of_nonempty` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder`	`sum`	—	`Multiset.sum_lt_sum_of_nonempty` `val_eq_zero` `not_nonempty_empty`
`sum_lt_sum_of_subset` 📖	mathematical	`Finset` `instHasSubset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE`	`sum`	—	`sum_insert` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `sum_le_sum_of_subset_of_nonneg` `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` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Monotone` `Finset` `partialOrder` `sum`	—	`sum_le_sum_of_subset_of_nonneg`
`sum_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty`	`sum`	—	`LT.lt.trans_le` `sum_lt_sum_of_nonempty` `sum_const_zero` `le_refl`
`sum_neg'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership` `Preorder.toLT`	`sum`	—	`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` `sum` `Finset` `instMembership`	—	`sum_pos_iff_of_nonneg` `OrderDual.addLeftMono`
`sum_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`le_trans` `sum_const_zero` `le_refl` `sum_le_sum`
`sum_nonneg'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`sum_nonneg`
`sum_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`LE.le.trans_eq` `sum_le_sum` `sum_const_zero`
`sum_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty`	`sum`	—	`lt_of_le_of_lt` `sum_const_zero` `le_refl` `sum_lt_sum_of_nonempty`
`sum_pos'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership` `Preorder.toLT`	`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` `instMembership`	—	`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` `sum` `Finset` `instMembership`	—	`sum_nonneg` `LE.le.lt_iff_ne'` `sum_eq_zero_iff_of_nonneg`
`sum_sdiff_le_sum_sdiff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `sum` `Finset` `instSDiff`	—	`add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `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` `PartialOrder.toPreorder` `Pi.instOne` `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`	`Finset.prod` `Finset.univ`	—	`Finset.one_lt_prod'` `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` `Finset.prod` `Finset.univ` `Pi.preorder`	—	`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`	—	`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`	—	`Finset.prod_eq_one_iff_of_one_le'`
`prod_le_one` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Finset.prod` `Finset.univ`	—	`Finset.prod_le_one'`
`prod_lt_one` 📖	mathematical	`Preorder.toLT` `Pi.preorder` `PartialOrder.toPreorder` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Finset.prod` `Finset.univ`	—	`Finset.prod_lt_one'` `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` `Finset.prod` `Finset.univ` `Pi.preorder`	—	`LE.le.eq_or_lt` `Finset.prod_congr` `Finset.prod_const_one`
`prod_mono'` 📖	mathematical	—	`Monotone` `Pi.preorder` `PartialOrder.toPreorder` `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'` `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`	—	`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`	—	`Finset.sum_eq_zero_iff_of_nonpos` `Finset.mem_univ`
`sum_mono` 📖	mathematical	—	`Monotone` `Pi.preorder` `PartialOrder.toPreorder` `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`	`Finset.sum` `Finset.univ`	—	`Finset.sum_neg'` `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` `Finset.sum` `Finset.univ` `Pi.preorder`	—	`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` `PartialOrder.toPreorder` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.sum` `Finset.univ`	—	`Finset.sum_nonneg`
`sum_nonpos` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.sum` `Finset.univ`	—	`Finset.sum_nonpos`
`sum_pos` 📖	mathematical	`Preorder.toLT` `Pi.preorder` `PartialOrder.toPreorder` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.sum` `Finset.univ`	—	`Finset.sum_pos'` `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` `Finset.sum` `Finset.univ` `Pi.preorder`	—	`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` `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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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` `instCanonicallyOrderedAdd` `mem_map_of_mem`
`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