Basic

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

Statistics

Metric	Count
Definitions `sumAddMonoidHom`	1
Theorems `map_multiset_ne_zero_sum`, `map_multiset_sum`, `map_multiset_prod`, `map_multiset_ne_zero_prod`, `coe_sumAddMonoidHom`, `dvd_prod`, `fst_prod`, `fst_sum`, `instIsAddTorsionFree`, `prod_add`, `prod_dvd_prod_of_dvd`, `prod_dvd_prod_of_le`, `prod_eq_one`, `prod_eq_pow_single`, `prod_erase`, `prod_filter_mul_prod_filter_not`, `prod_hom`, `prod_hom'`, `prod_hom_ne_zero`, `prod_hom₂`, `prod_hom₂_ne_zero`, `prod_int_mod`, `prod_map_div`, `prod_map_eq_pow_single`, `prod_map_erase`, `prod_map_inv`, `prod_map_inv'`, `prod_map_mul`, `prod_map_pow`, `prod_map_prod_map`, `prod_map_zpow`, `prod_nat_mod`, `prod_nsmul`, `snd_prod`, `snd_sum`, `sum_add`, `sum_eq_nsmul_single`, `sum_eq_zero`, `sum_erase`, `sum_filter_add_sum_filter_not`, `sum_hom`, `sum_hom'`, `sum_hom_ne_zero`, `sum_hom₂`, `sum_hom₂_ne_zero`, `sum_int_mod`, `sum_map_add`, `sum_map_eq_nsmul_single`, `sum_map_erase`, `sum_map_neg`, `sum_map_neg'`, `sum_map_nsmul`, `sum_map_singleton`, `sum_map_sub`, `sum_map_sum_map`, `sum_map_tsub`, `sum_map_zsmul`, `sum_nat_mod`, `sum_nsmul`, `map_multiset_ne_zero_prod`, `map_multiset_ne_zero_sum`, `map_multiset_prod`, `map_multiset_sum`	63
Total	64

AddHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_multiset_ne_zero_sum` 📖	mathematical	—	`DFunLike.coe` `AddHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `funLike` `Multiset.sum` `Multiset.map`	—	`Multiset.sum_hom_ne_zero` `addHomClass`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_multiset_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `Multiset.sum` `Multiset.map`	—	`Multiset.sum_hom` `instAddMonoidHomClass`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_multiset_prod` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instFunLike` `Multiset.prod` `Multiset.map`	—	`Multiset.prod_hom` `instMonoidHomClass`

MulHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_multiset_ne_zero_prod` 📖	mathematical	—	`DFunLike.coe` `MulHom` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `funLike` `Multiset.prod` `Multiset.map`	—	`Multiset.prod_hom_ne_zero` `mulHomClass`

Multiset

Definitions

Name	Category	Theorems
`sumAddMonoidHom` 📖	CompOp	1 math math: `coe_sumAddMonoidHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_sumAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Multiset` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `sumAddMonoidHom` `sum`	—	—
`dvd_prod` 📖	mathematical	`Multiset` `instMembership`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `prod`	—	`List.dvd_prod`
`fst_prod` 📖	mathematical	—	`prod` `Prod.instCommMonoid` `map`	—	`map_multiset_prod` `MonoidHom.instMonoidHomClass`
`fst_sum` 📖	mathematical	—	`sum` `Prod.instAddCommMonoid` `map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`instIsAddTorsionFree` 📖	mathematical	—	`IsAddTorsionFree` `Multiset` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid`	—	`ext'` `count.congr_simp`
`prod_add` 📖	mathematical	—	`prod` `Multiset` `instAdd` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative`
`prod_dvd_prod_of_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	`prod` `map`	—	`induction_on'` `map_cons` `prod_cons` `mul_dvd_mul`
`prod_dvd_prod_of_le` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `prod`	—	`ExistsAddOfLE.exists_add_of_le` `instExistsAddOfLE` `prod_add`
`prod_eq_one` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod`	—	`List.prod_eq_one`
`prod_eq_pow_single` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `Monoid.toNatPow` `count`	—	`List.prod_eq_pow_single` `coe_count`
`prod_erase` 📖	mathematical	`Multiset` `instMembership`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `erase`	—	`coe_toList` `coe_erase` `prod_coe` `List.prod_erase` `mem_toList`
`prod_filter_mul_prod_filter_not` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `filter`	—	`prod_add` `filter_add_not`
`prod_hom` 📖	mathematical	—	`prod` `map` `DFunLike.coe`	—	`List.prod_hom`
`prod_hom'` 📖	mathematical	—	`prod` `map` `DFunLike.coe`	—	`map_map` `prod_hom`
`prod_hom_ne_zero` 📖	mathematical	—	`prod` `map` `DFunLike.coe`	—	`List.prod_hom_nonempty`
`prod_hom₂` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne`	`prod` `map`	—	`List.prod_hom₂`
`prod_hom₂_ne_zero` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `map`	—	`List.prod_hom₂_nonempty`
`prod_int_mod` 📖	mathematical	—	`prod` `Int.instCommMonoid` `map`	—	`induction` `prod_cons` `map_cons`
`prod_map_div` 📖	mathematical	—	`prod` `DivisionCommMonoid.toCommMonoid` `map` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`prod_hom₂` `mul_div_mul_comm` `div_one`
`prod_map_eq_pow_single` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `map` `Monoid.toNatPow` `count`	—	`List.prod_map_eq_pow_single` `coe_count`
`prod_map_erase` 📖	mathematical	`Multiset` `instMembership`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `prod` `map` `erase`	—	`coe_toList` `coe_erase` `map_coe` `prod_coe` `List.prod_map_erase` `mem_toList`
`prod_map_inv` 📖	mathematical	—	`prod` `DivisionCommMonoid.toCommMonoid` `map` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`prod_map_inv'` `map_map`
`prod_map_inv'` 📖	mathematical	—	`prod` `DivisionCommMonoid.toCommMonoid` `map` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`prod_hom` `MonoidHom.instMonoidHomClass`
`prod_map_mul` 📖	mathematical	—	`prod` `map` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`prod_hom₂` `mul_mul_mul_comm` `mul_one`
`prod_map_pow` 📖	mathematical	—	`prod` `map` `Monoid.toNatPow` `CommMonoid.toMonoid`	—	`prod_hom'` `MonoidHom.instMonoidHomClass`
`prod_map_prod_map` 📖	mathematical	—	`prod` `map`	—	`induction_on` `map_congr` `map_const'` `prod_replicate` `one_pow` `map_cons` `prod_cons` `prod_map_mul`
`prod_map_zpow` 📖	mathematical	—	`prod` `DivisionCommMonoid.toCommMonoid` `map` `DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid`	—	`map_congr` `map_map` `prod_hom` `MonoidHom.instMonoidHomClass`
`prod_nat_mod` 📖	mathematical	—	`prod` `Nat.instCommMonoid` `map`	—	`induction` `prod_cons` `map_cons`
`prod_nsmul` 📖	mathematical	—	`prod` `Multiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `Monoid.toNatPow` `CommMonoid.toMonoid`	—	`zero_nsmul` `pow_zero` `add_nsmul` `one_nsmul` `pow_add` `pow_one` `prod_add`
`snd_prod` 📖	mathematical	—	`prod` `Prod.instCommMonoid` `map`	—	`map_multiset_prod` `MonoidHom.instMonoidHomClass`
`snd_sum` 📖	mathematical	—	`sum` `Prod.instAddCommMonoid` `map`	—	`map_multiset_sum` `AddMonoidHom.instAddMonoidHomClass`
`sum_add` 📖	mathematical	—	`sum` `Multiset` `instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative`
`sum_eq_nsmul_single` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `AddMonoid.toNatSMul` `count`	—	`List.sum_eq_nsmul_single` `coe_count`
`sum_eq_zero` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum`	—	`List.sum_eq_zero`
`sum_erase` 📖	mathematical	`Multiset` `instMembership`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `erase`	—	`coe_toList` `coe_erase` `sum_coe` `List.sum_erase` `mem_toList`
`sum_filter_add_sum_filter_not` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `filter`	—	`sum_add` `filter_add_not`
`sum_hom` 📖	mathematical	—	`sum` `map` `DFunLike.coe`	—	`List.sum_hom`
`sum_hom'` 📖	mathematical	—	`sum` `map` `DFunLike.coe`	—	`map_map` `sum_hom`
`sum_hom_ne_zero` 📖	mathematical	—	`sum` `map` `DFunLike.coe`	—	`List.sum_hom_nonempty` `coe_eq_zero`
`sum_hom₂` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero`	`sum` `map`	—	`List.sum_hom₂`
`sum_hom₂_ne_zero` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `map`	—	`List.sum_hom₂_nonempty` `coe_eq_zero`
`sum_int_mod` 📖	mathematical	—	`sum` `Int.instAddCommMonoid` `map`	—	`induction` `sum_cons` `map_cons`
`sum_map_add` 📖	mathematical	—	`sum` `map` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`sum_hom₂` `add_add_add_comm` `add_zero`
`sum_map_eq_nsmul_single` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `map` `AddMonoid.toNatSMul` `count`	—	`List.sum_map_eq_nsmul_single` `coe_count`
`sum_map_erase` 📖	mathematical	`Multiset` `instMembership`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `map` `erase`	—	`coe_toList` `coe_erase` `map_coe` `sum_coe` `List.sum_map_erase` `mem_toList`
`sum_map_neg` 📖	mathematical	—	`sum` `SubtractionCommMonoid.toAddCommMonoid` `map` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	—	`sum_map_neg'` `map_map`
`sum_map_neg'` 📖	mathematical	—	`sum` `SubtractionCommMonoid.toAddCommMonoid` `map` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	—	`sum_hom` `AddMonoidHom.instAddMonoidHomClass`
`sum_map_nsmul` 📖	mathematical	—	`sum` `map` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`sum_hom'` `AddMonoidHom.instAddMonoidHomClass`
`sum_map_singleton` 📖	mathematical	—	`sum` `Multiset` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `map` `instSingleton`	—	`induction_on` `map_cons` `sum_cons`
`sum_map_sub` 📖	mathematical	—	`sum` `SubtractionCommMonoid.toAddCommMonoid` `map` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	—	`sum_hom₂` `add_sub_add_comm` `sub_zero`
`sum_map_sum_map` 📖	mathematical	—	`sum` `map`	—	`induction_on` `map_congr` `map_const'` `sum_replicate` `nsmul_zero` `map_cons` `sum_cons` `sum_map_add`
`sum_map_tsub` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`sum` `map`	—	`eq_tsub_of_add_eq` `sum_map_add` `map_congr` `tsub_add_cancel_of_le`
`sum_map_zsmul` 📖	mathematical	—	`sum` `SubtractionCommMonoid.toAddCommMonoid` `map` `SubNegMonoid.toZSMul` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid`	—	`map_congr` `map_map` `sum_hom` `AddMonoidHom.instAddMonoidHomClass`
`sum_nat_mod` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `map`	—	`induction` `sum_cons` `map_cons`
`sum_nsmul` 📖	mathematical	—	`sum` `Multiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid`	—	`zero_nsmul` `add_nsmul` `one_nsmul` `sum_add`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_multiset_ne_zero_prod` 📖	mathematical	—	`DFunLike.coe` `Multiset.prod` `Multiset.map`	—	`Multiset.prod_hom_ne_zero`
`map_multiset_ne_zero_sum` 📖	mathematical	—	`DFunLike.coe` `Multiset.sum` `Multiset.map`	—	`Multiset.sum_hom_ne_zero`
`map_multiset_prod` 📖	mathematical	—	`DFunLike.coe` `Multiset.prod` `Multiset.map`	—	`Multiset.prod_hom`
`map_multiset_sum` 📖	mathematical	—	`DFunLike.coe` `Multiset.sum` `Multiset.map`	—	`Multiset.sum_hom`

---

← Back to Index