Multiset

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

Statistics

Metric	Count
Definitions	0
Theorems `abs_sum_le_sum_abs`, `all_one_of_le_one_le_of_prod_eq_one`, `all_zero_of_le_zero_le_of_sum_eq_zero`, `apply_prod_le_sum_map`, `card_nsmul_le_sum`, `le_prod_nonempty_of_submultiplicative`, `le_prod_nonempty_of_submultiplicative_on_pred`, `le_prod_of_mem`, `le_prod_of_submultiplicative`, `le_prod_of_submultiplicative_on_pred`, `le_sum_nonempty_of_subadditive`, `le_sum_nonempty_of_subadditive_on_pred`, `le_sum_of_mem`, `le_sum_of_subadditive`, `le_sum_of_subadditive_on_pred`, `max_le_of_forall_le`, `max_prod_le`, `max_sum_le`, `one_le_prod_of_one_le`, `pow_card_le_prod`, `prod_eq_one_iff`, `prod_le_pow_card`, `prod_le_prod_map`, `prod_le_prod_of_rel_le`, `prod_lt_prod'`, `prod_lt_prod_of_nonempty'`, `prod_map_le_prod`, `prod_map_le_prod_map`, `prod_min_le`, `single_le_prod`, `single_le_sum`, `sum_eq_zero_iff`, `sum_le_card_nsmul`, `sum_le_sum_map`, `sum_le_sum_of_rel_le`, `sum_lt_sum`, `sum_lt_sum_of_nonempty`, `sum_map_le_apply_prod`, `sum_map_le_sum`, `sum_map_le_sum_map`, `sum_min_le`, `sum_nonneg`	42
Total	42

Multiset

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` `map`	—	`le_sum_of_subadditive` `Eq.le` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `abs_add_le`
`all_one_of_le_one_le_of_prod_eq_one` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `Multiset` `instMembership`	—	—	`List.all_one_of_le_one_le_of_prod_eq_one`
`all_zero_of_le_zero_le_of_sum_eq_zero` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `Multiset` `instMembership`	—	—	`mem_coe` `List.all_zero_of_le_zero_le_of_sum_eq_zero`
`apply_prod_le_sum_map` 📖	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` `map`	—	`List.apply_prod_le_sum_map`
`card_nsmul_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card` `sum`	—	`sum_replicate` `map_const` `sum_map_le_sum`
`le_prod_nonempty_of_submultiplicative` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `map`	—	`List.le_prod_nonempty_of_submultiplicative`
`le_prod_nonempty_of_submultiplicative_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `map`	—	`List.le_prod_nonempty_of_submultiplicative_on_pred`
`le_prod_of_mem` 📖	mathematical	`Multiset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `prod`	—	`exists_cons_of_mem` `prod_cons` `le_mul_right` `le_refl`
`le_prod_of_submultiplicative` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	`prod` `map`	—	`List.le_prod_of_submultiplicative`
`le_prod_of_submultiplicative_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	`prod` `map`	—	`List.le_prod_of_submultiplicative_on_pred`
`le_sum_nonempty_of_subadditive` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `map`	—	`List.le_sum_nonempty_of_subadditive` `coe_eq_zero`
`le_sum_nonempty_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `map`	—	`List.le_sum_nonempty_of_subadditive_on_pred` `coe_eq_zero`
`le_sum_of_mem` 📖	mathematical	`Multiset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `sum`	—	`exists_cons_of_mem` `sum_cons` `le_add_right` `le_refl`
`le_sum_of_subadditive` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	`sum` `map`	—	`List.le_sum_of_subadditive`
`le_sum_of_subadditive_on_pred` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	`sum` `map`	—	`List.le_sum_of_subadditive_on_pred`
`max_le_of_forall_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`fold` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instCommutativeMax` `instAssociativeMax` `Bot.bot` `OrderBot.toBot`	—	`instCommutativeMax` `instAssociativeMax` `List.max_le_of_forall_le`
`max_prod_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `prod` `map`	—	`List.max_prod_le` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`max_sum_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `sum` `map`	—	`List.max_sum_le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`one_le_prod_of_one_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`List.one_le_prod_of_one_le`
`pow_card_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`Monoid.toNatPow` `CommMonoid.toMonoid` `card` `prod`	—	`prod_replicate` `map_const` `prod_map_le_prod`
`prod_eq_one_iff` 📖	mathematical	—	`prod` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`List.prod_eq_one_iff`
`prod_le_pow_card` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod` `Monoid.toNatPow` `CommMonoid.toMonoid` `card`	—	`List.prod_le_pow_card` `covariant_swap_mul_of_covariant_mul`
`prod_le_prod_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod` `map`	—	`prod_map_le_prod` `OrderDual.mulLeftMono`
`prod_le_prod_of_rel_le` 📖	mathematical	`Rel` `Preorder.toLE` `PartialOrder.toPreorder`	`prod`	—	`le_refl` `prod_cons` `mul_le_mul'` `covariant_swap_mul_of_covariant_mul`
`prod_lt_prod'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Multiset` `instMembership` `Preorder.toLT`	`prod` `map`	—	`List.prod_lt_prod'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul`
`prod_lt_prod_of_nonempty'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`prod` `map`	—	`exists_mem_of_ne_zero` `prod_lt_prod'` `le_of_lt`
`prod_map_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod` `map`	—	`prod_le_prod_of_rel_le` `rel_map_left` `rel_refl_of_refl_on`
`prod_map_le_prod_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`prod` `map`	—	`prod_le_prod_of_rel_le` `rel_map` `rel_refl_of_refl_on`
`prod_min_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `prod` `map` `SemilatticeInf.toMin`	—	`List.prod_min_le` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`single_le_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Multiset` `instMembership`	`prod`	—	`List.single_le_prod`
`single_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Multiset` `instMembership`	`sum`	—	`List.single_le_sum`
`sum_eq_zero_iff` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`mem_coe` `List.sum_eq_zero_iff`
`sum_le_card_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	—	`List.sum_le_card_nsmul` `covariant_swap_add_of_covariant_add`
`sum_le_sum_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `map`	—	`sum_map_le_sum` `OrderDual.addLeftMono`
`sum_le_sum_of_rel_le` 📖	mathematical	`Rel` `Preorder.toLE` `PartialOrder.toPreorder`	`sum`	—	`le_refl` `sum_cons` `add_le_add` `covariant_swap_add_of_covariant_add`
`sum_lt_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Multiset` `instMembership` `Preorder.toLT`	`sum` `map`	—	`List.sum_lt_sum` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`sum_lt_sum_of_nonempty` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`sum` `map`	—	`exists_mem_of_ne_zero` `sum_lt_sum` `le_of_lt`
`sum_map_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` `map` `prod`	—	`apply_prod_le_sum_map` `OrderDual.addLeftMono`
`sum_map_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `map`	—	`sum_le_sum_of_rel_le` `rel_map_left` `rel_refl_of_refl_on`
`sum_map_le_sum_map` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `map`	—	`sum_le_sum_of_rel_le` `rel_map` `rel_refl_of_refl_on`
`sum_min_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `map` `SemilatticeInf.toMin`	—	`List.sum_min_le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`sum_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`List.sum_nonneg`

---

← Back to Index