Nat

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

Statistics

Metric	Count
Definitions	0
Theorems factors_eq, factors_multiset_prod_of_irreducible, instUniqueFactorizationMonoid, instWfDvdMonoid	4
Total	4

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factors_eq 📖	mathematical	—	UniqueFactorizationMonoid.normalizedFactors instCommMonoidWithZero NormalizationMonoid.ofUniqueUnits Unique.instSubsingleton Units MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero unique_units instUniqueFactorizationMonoid Multiset.ofList primeFactorsList	—	Unique.instSubsingleton instUniqueFactorizationMonoid UniqueFactorizationMonoid.normalizedFactors_zero primeFactorsList_zero Multiset.rel_eq associated_eq_eq UniqueFactorizationMonoid.factors_unique UniqueFactorizationMonoid.irreducible_of_normalized_factor irreducible_iff_prime prime_iff prime_of_mem_primeFactorsList Multiset.prod_coe prod_primeFactorsList UniqueFactorizationMonoid.prod_normalizedFactors
factors_multiset_prod_of_irreducible 📖	mathematical	Irreducible instMonoid	UniqueFactorizationMonoid.normalizedFactors instCommMonoidWithZero NormalizationMonoid.ofUniqueUnits Unique.instSubsingleton Units MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero unique_units instUniqueFactorizationMonoid Multiset.prod instCommMonoid	—	Unique.instSubsingleton instUniqueFactorizationMonoid Multiset.rel_eq associated_eq_eq UniqueFactorizationMonoid.factors_unique UniqueFactorizationMonoid.irreducible_of_normalized_factor UniqueFactorizationMonoid.prod_normalizedFactors Multiset.prod_eq_zero_iff IsDomain.to_noZeroDivisors instIsDomain instNontrivial not_irreducible_zero
instUniqueFactorizationMonoid 📖	mathematical	—	UniqueFactorizationMonoid instCommMonoidWithZero	—	instIsCancelMulZero instWfDvdMonoid irreducible_iff_prime
instWfDvdMonoid 📖	mathematical	—	WfDvdMonoid instCommMonoidWithZero	—	RelHomClass.wellFounded RelHom.instRelHomClass Unique.instSubsingleton MulZeroClass.zero_mul cast_add cast_one dvd_and_not_dvd_iff instIsCancelMulZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass lt_of_le_of_ne dvd_refl wellFounded_lt

---

← Back to Index