Documentation Verification Report

Associated

📁 Source: Mathlib/Algebra/BigOperators/Associated.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod`, `exists_mem_multiset_le_of_prime`, `finset_prod_mk`, `prod_eq_one_iff`, `prod_le_prod`, `prod_mk`, `rel_associated_iff_map_eq_map`, `prod_primes_dvd`, `prod_ne_zero_of_prime`, `prod_primes_dvd`, `dvd_finset_prod_iff`, `dvd_finsuppProd_iff`, `exists_mem_finset_dvd`, `exists_mem_multiset_dvd`, `exists_mem_multiset_map_dvd`, `not_dvd_finset_prod`, `not_dvd_finsuppProd`, `associated_iff`, `divisor_closure_eq_closure`, `exists_associated_mem_of_dvd_prod`	20
Total	20

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`Associated` `CommMonoid.toMonoid`	`Finset.prod`	—	`Finset.induction` `refl`

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_multiset_le_of_prime` 📖	mathematical	`Prime` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid` `Multiset.prod` `instCommMonoid`	`Multiset` `Multiset.instMembership`	—	`Multiset.induction_on` `Prime.ne_one` `mul_eq_one` `Unique.instSubsingleton` `Multiset.prod_cons` `Prime.le_or_le` `Multiset.mem_cons_self` `Multiset.mem_cons_of_mem`
`finset_prod_mk` 📖	mathematical	—	`Finset.prod` `Associates` `CommMonoid.toMonoid` `instCommMonoid`	—	`Finset.prod_eq_multiset_prod` `Multiset.map_map`
`prod_eq_one_iff` 📖	mathematical	—	`Multiset.prod` `Associates` `CommMonoid.toMonoid` `instCommMonoid` `instOne`	—	`Multiset.induction_on` `instIsEmptyFalse` `Multiset.prod_cons` `Unique.instSubsingleton`
`prod_le_prod` 📖	mathematical	`Multiset` `Associates` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	`instPreorder` `Multiset.prod` `instCommMonoid`	—	`mul_mono` `le_refl` `one_le` `Multiset.prod_add` `mul_one` `add_tsub_cancel_of_le` `Multiset.instExistsAddOfLE` `Multiset.instAddLeftMono` `Multiset.instOrderedSub`
`prod_mk` 📖	mathematical	—	`Multiset.prod` `Associates` `CommMonoid.toMonoid` `instCommMonoid` `Multiset.map`	—	`Multiset.induction_on` `Multiset.map_cons` `Multiset.prod_cons`
`rel_associated_iff_map_eq_map` 📖	mathematical	—	`Multiset.Rel` `Associated` `CommMonoid.toMonoid` `Multiset.map` `Associates`	—	`Multiset.rel_eq` `Multiset.rel_map`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_primes_dvd` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`Multiset.prod_primes_dvd` `IsCancelMulZero.toIsLeftCancelMulZero` `Multiset.map_id'` `Multiset.countP_congr` `associated_eq_eq` `Multiset.countP_eq_card_filter` `Multiset.count_eq_card_filter_eq` `nodup`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_ne_zero_of_prime` 📖	—	`Prime`	—	—	`prod_ne_zero` `Prime.ne_zero`
`prod_primes_dvd` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `countP` `Associated` `MonoidWithZero.toMonoid`	`prod` `CommMonoidWithZero.toCommMonoid`	—	`induction_on` `prod_cons` `mem_cons_self` `mul_dvd_mul_left` `mem_cons_of_mem` `Prime.dvd_or_dvd` `Prime.associated_of_dvd` `countP_pos` `not_lt` `countP_cons_of_pos` `Associated.refl` `Associated.symm` `LE.le.trans` `countP_le_of_le` `le_cons_self`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_finset_prod_iff` 📖	mathematical	`Prime`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Finset.prod` `CommMonoidWithZero.toCommMonoid` `Finset` `Finset.instMembership`	—	`exists_mem_finset_dvd` `dvd_trans` `Finset.dvd_prod_of_mem`
`dvd_finsuppProd_iff` 📖	mathematical	`Prime` `Nat.instCommMonoidWithZero`	`Finsupp.prod` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Nat.instCommMonoid` `Finset` `Finset.instMembership` `Finsupp.support` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike`	—	`dvd_finset_prod_iff`
`exists_mem_finset_dvd` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Finset.prod` `CommMonoidWithZero.toCommMonoid`	`Finset` `Finset.instMembership`	—	`exists_mem_multiset_map_dvd`
`exists_mem_multiset_dvd` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Multiset` `Multiset.instMembership`	—	`Multiset.induction_on` `not_dvd_one` `Multiset.prod_cons` `dvd_or_dvd` `Multiset.mem_cons_self` `Multiset.mem_cons_of_mem`
`exists_mem_multiset_map_dvd` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.map`	`Multiset` `Multiset.instMembership`	—	`exists_mem_multiset_dvd`
`not_dvd_finset_prod` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`Finset.prod` `CommMonoidWithZero.toCommMonoid`	—	`dvd_finset_prod_iff`
`not_dvd_finsuppProd` 📖	mathematical	`Prime` `Nat.instCommMonoidWithZero` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finsupp.instFunLike`	`Finsupp.prod` `Nat.instCommMonoid`	—	`not_dvd_finset_prod`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_iff` 📖	mathematical	—	`Associated` `instMonoid`	—	`eq_iff_fst_eq_snd_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divisor_closure_eq_closure` 📖	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure` `setOf` `IsUnit` `MonoidWithZero.toMonoid` `Prime` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass`	—	—	`Submonoid.exists_multiset_of_mem_closure` `Multiset.induction` `Submonoid.subset_closure` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `IsUnit.exists_right_inv` `Multiset.prod_cons` `mul_comm` `Submonoid.multiset_prod_mem` `Multiset.forall_mem_cons` `IsUnit.of_mul_eq_one_right` `mul_one` `mul_assoc` `mul_eq_mul_right_iff` `IsCancelMulZero.toIsRightCancelMulZero` `Prime.dvd_mul` `Dvd.intro` `Submonoid.mul_mem` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Prime.ne_zero`
`exists_associated_mem_of_dvd_prod` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Multiset` `Multiset.instMembership` `Associated` `MonoidWithZero.toMonoid`	—	`Multiset.induction_on` `instIsEmptyFalse` `isUnit_iff_dvd_one` `Prime.not_unit` `Zero.instNonempty` `Prime.dvd_or_dvd` `Multiset.prod_cons` `Multiset.mem_cons` `Multiset.mem_cons_self` `Prime.associated_of_dvd`

---

← Back to Index