Documentation Verification Report

Multiplicity

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Statistics

Metric	Count
Definitions	0
Theorems `of_not_isUnit`, `of_prime_left`, `count_normalizedFactors_eq`, `count_normalizedFactors_eq'`, `emultiplicity_eq_count_normalizedFactors`, `le_emultiplicity_iff_replicate_le_normalizedFactors`, `max_power_factor`, `max_power_factor'`	8
Total	8

FiniteMultiplicity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_not_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`FiniteMultiplicity`	—	`WfDvdMonoid.max_power_factor'` `pow_succ` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `left_ne_zero_of_mul`
`of_prime_left` 📖	mathematical	`Prime`	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`of_not_isUnit` `Prime.not_unit`

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_normalizedFactors_eq` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow`	`Multiset.count` `normalizedFactors`	—	`Nat.cast_injective` `emultiplicity_eq_coe` `emultiplicity_eq_count_normalizedFactors`
`count_normalizedFactors_eq'` 📖	mathematical	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `MonoidWithZero.toMonoid` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `normalize` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow`	`Multiset.count` `normalizedFactors`	—	`Multiset.count_eq_zero` `zero_notMem_normalizedFactors` `zero_pow` `count_normalizedFactors_eq`
`emultiplicity_eq_count_normalizedFactors` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`emultiplicity` `ENat` `ENat.instNatCast` `Multiset.count` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize` `normalizedFactors`	—	`le_antisymm` `Order.le_of_lt_add_one` `Nat.cast_one` `Nat.cast_add` `lt_iff_not_ge` `le_emultiplicity_iff_replicate_le_normalizedFactors` `Multiset.le_count_iff_replicate_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `le_refl`
`le_emultiplicity_iff_replicate_le_normalizedFactors` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity` `Multiset` `Multiset.instPartialOrder` `Multiset.replicate` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize` `normalizedFactors`	—	`pow_dvd_iff_le_emultiplicity` `pow_zero` `Multiset.instCanonicallyOrderedAdd` `pow_succ'` `mul_assoc` `normalizedFactors_mul` `mul_eq_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `Multiset.replicate_succ` `normalizedFactors_irreducible` `Multiset.singleton_add` `Multiset.cons_le_cons_iff` `Dvd.intro` `Multiset.le_iff_exists_add` `Associated.dvd_iff_dvd_right` `prod_normalizedFactors` `Multiset.prod_add` `Multiset.prod_replicate` `Dvd.dvd.trans` `Associated.dvd` `Associated.pow_pow` `associated_normalize`

WfDvdMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`max_power_factor` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow`	—	`max_power_factor'` `Irreducible.not_isUnit`
`max_power_factor'` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow`	—	`WellFounded.has_min` `wellFounded_dvdNotUnit` `pow_zero` `one_mul` `pow_succ` `mul_assoc` `right_ne_zero_of_mul` `mul_comm`

---

← Back to Index