Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `UniqueFactorizationMonoid`, `WfDvdMonoid`	2
Theorems `card_factors_of_irreducible`, `dvd_of_mem_factors`, `exists_prime_factors`, `exists_prime_iff`, `factors_prod`, `factors_zero`, `induction_on_prime`, `instDecompositionMonoid`, `irreducible_iff_prime`, `irreducible_of_factor`, `ne_zero_of_mem_factors`, `prime_of_factor`, `toIsCancelMulZero`, `toIsWellFounded`, `exists_factors`, `exists_irreducible_factor`, `induction_on_irreducible`, `isRelPrime_of_no_irreducible_factors`, `not_unit_iff_exists_factors_eq`, `ufm_of_decomposition_of_wfDvdMonoid`, `wellFounded_dvdNotUnit`	21
Total	23

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_factors_of_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Multiset.card` `factors`	—	`Irreducible.not_isUnit` `factors_prod` `Irreducible.ne_zero` `Multiset.exists_mem_of_ne_zero` `Multiset.exists_cons_of_mem` `Multiset.card_cons` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `Multiset.card_eq_zero` `Multiset.eq_zero_iff_forall_notMem` `irreducible_of_factor` `Multiset.mem_cons_of_mem` `Associated.irreducible_iff` `Multiset.prod_cons` `instIsDedekindFiniteMonoid`
`dvd_of_mem_factors` 📖	mathematical	`Multiset` `Multiset.instMembership` `factors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`dvd_trans` `Multiset.dvd_prod` `Associated.dvd` `factors_prod` `ne_zero_of_mem_factors`
`exists_prime_factors` 📖	mathematical	—	`Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	—	`WfDvdMonoid.exists_factors` `toIsWellFounded`
`exists_prime_iff` 📖	mathematical	—	`Prime` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.ne_zero` `Prime.not_unit` `WfDvdMonoid.exists_irreducible_factor` `toIsWellFounded` `irreducible_iff_prime`
`factors_prod` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `factors`	—	`exists_prime_factors` `factors.eq_1`
`factors_zero` 📖	mathematical	—	`factors` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instZero`	—	`exists_prime_factors`
`induction_on_prime` 📖	—	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul`	—	—	`WfDvdMonoid.induction_on_irreducible` `toIsWellFounded`
`instDecompositionMonoid` 📖	mathematical	—	`DecompositionMonoid` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`eq_or_ne` `isPrimal_zero` `exists_prime_factors` `IsPrimal.mul` `toIsCancelMulZero` `Submonoid.multiset_prod_mem` `Prime.isPrimal` `IsUnit.isPrimal` `Units.isUnit`
`irreducible_iff_prime` 📖	mathematical	—	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime`	—	—
`irreducible_of_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `factors`	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.irreducible` `toIsCancelMulZero` `prime_of_factor`
`ne_zero_of_mem_factors` 📖	—	`Multiset` `Multiset.instMembership` `factors`	—	—	`factors_zero`
`prime_of_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `factors`	`Prime`	—	`ne_zero_of_mem_factors` `exists_prime_factors` `factors.eq_1`
`toIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toZero`	—	—
`toIsWellFounded` 📖	mathematical	—	`IsWellFounded` `DvdNotUnit`	—	—

WfDvdMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_factors` 📖	mathematical	—	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associated` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	—	`induction_on_irreducible` `Multiset.notMem_zero` `one_mul` `Multiset.mem_cons` `Multiset.prod_cons` `Associated.mul_left`
`exists_irreducible_factor` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Irreducible` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`WellFounded.has_min` `wellFounded_dvdNotUnit` `dvd_rfl` `dvd_trans` `of_not_not` `ne_zero_of_dvd_ne_zero`
`induction_on_irreducible` 📖	—	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul`	—	—	`wellFounded_dvdNotUnit` `exists_irreducible_factor` `ne_zero_of_dvd_ne_zero` `mul_comm` `Irreducible.not_isUnit`
`isRelPrime_of_no_irreducible_factors` 📖	mathematical	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`IsRelPrime` `MonoidWithZero.toMonoid`	—	`isRelPrime_of_no_nonunits_factors` `exists_irreducible_factor` `Dvd.dvd.trans`
`not_unit_iff_exists_factors_eq` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	—	`exists_factors` `Multiset.exists_mem_of_ne_zero` `one_mul` `Multiset.mem_cons` `Associated.irreducible` `Multiset.mem_of_mem_erase` `Multiset.prod_cons` `mul_comm` `mul_assoc` `Multiset.prod_erase` `Multiset.cons_ne_zero` `not_isUnit_of_not_isUnit_dvd` `Irreducible.not_isUnit` `Multiset.dvd_prod`

(root)

Definitions

Name	Category	Theorems
`UniqueFactorizationMonoid` 📖	CompData	17 math math: `PowerSeries.instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain`, `IsBezout.TFAE`, `MulEquiv.uniqueFactorizationMonoid_iff`, `MvPolynomial.uniqueFactorizationMonoid`, `PowerSeries.instUniqueFactorizationMonoid`, `PrincipalIdealRing.to_uniqueFactorizationMonoid`, `Nat.instUniqueFactorizationMonoid`, `IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid`, `Associates.ufm`, `UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime`, `ufm_of_decomposition_of_wfDvdMonoid`, `UniqueFactorizationMonoid.iff_exists_prime_factors`, `Polynomial.uniqueFactorizationMonoid`, `Ideal.uniqueFactorizationMonoid`, `MulEquiv.uniqueFactorizationMonoid`, `UniqueFactorizationMonoid.of_existsUnique_irreducible_factors`, `UniqueFactorizationMonoid.of_exists_prime_factors`
`WfDvdMonoid` 📖	MathDef	12 math math: `IsBezout.TFAE`, `WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt`, `instWfDvdMonoidIdeal`, `WfDvdMonoid.of_wellFoundedLT_associates`, `WfDvdMonoid.wfDvdMonoid_associates`, `Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v`, `IsNoetherianRing.wfDvdMonoid`, `Nat.instWfDvdMonoid`, `WfDvdMonoid.iff_wellFounded_associates`, `WfDvdMonoid.of_exists_prime_factors`, `Polynomial.wfDvdMonoid`, `WfDvdMonoid.of_wfDvdMonoid_associates`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ufm_of_decomposition_of_wfDvdMonoid` 📖	mathematical	—	`UniqueFactorizationMonoid`	—	`irreducible_iff_prime`
`wellFounded_dvdNotUnit` 📖	mathematical	—	`DvdNotUnit`	—	`IsWellFounded.wf`

---

← Back to Index