Documentation Verification Report

Multiset

📁 Source: Mathlib/Algebra/BigOperators/Ring/Multiset.lean

Statistics

Metric	Count
Definitions	0
Theorems `multiset_sum_left`, `multiset_sum_right`, `dvd_sum`, `prod_eq_zero`, `prod_eq_zero_iff`, `prod_map_add`, `prod_map_neg`, `prod_map_sum`, `prod_ne_zero`, `sum_map_mul_left`, `sum_map_mul_right`	11
Total	11

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multiset_sum_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`symm` `multiset_sum_right`
`multiset_sum_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Multiset.quot_mk_to_coe` `Multiset.sum_coe` `list_sum_right`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_sum` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`induction_on` `dvd_zero` `sum_cons` `dvd_add` `Distrib.leftDistribClass` `mem_cons_self` `mem_cons`
`prod_eq_zero` 📖	mathematical	`Multiset` `instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`exists_cons_of_mem` `prod_cons` `MulZeroClass.zero_mul`
`prod_eq_zero_iff` 📖	mathematical	—	`prod` `CommMonoidWithZero.toCommMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `instMembership`	—	`quot_mk_to_coe` `prod_coe` `List.prod_eq_zero_iff`
`prod_map_add` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `map` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Multiset` `Distrib.toMul` `antidiagonal`	—	`induction_on` `mul_one` `sum_singleton` `map_cons` `prod_cons` `sum_map_mul_left` `map_congr` `add_mul` `Distrib.rightDistribClass` `mul_left_comm` `sum_map_add` `antidiagonal_cons` `map_add` `map_map` `mul_assoc` `sum_add` `add_comm`
`prod_map_neg` 📖	mathematical	—	`prod` `map` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Monoid.toNatPow` `MulOne.toOne` `card`	—	`List.prod_map_neg`
`prod_map_sum` 📖	mathematical	—	`prod` `CommSemiring.toCommMonoid` `map` `Multiset` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Sections`	—	`induction_on` `sum_singleton` `map_cons` `prod_cons` `map_congr` `sections_cons` `map_bind` `map_map` `sum_bind` `sum_map_mul_left` `sum_map_mul_right` `map_id'`
`prod_ne_zero` 📖	—	`Multiset` `instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	—	`prod_eq_zero_iff`
`sum_map_mul_left` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`induction_on` `MulZeroClass.mul_zero` `map_cons` `sum_cons` `mul_add` `Distrib.leftDistribClass`
`sum_map_mul_right` 📖	mathematical	—	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`induction_on` `MulZeroClass.zero_mul` `map_cons` `sum_cons` `add_mul` `Distrib.rightDistribClass`

---

← Back to Index