Commit 2025-06-01 19:52 cf132bfd

View on Github →

feat(RingTheory/Radical): generalise and fill in TODOs (#25335)

Generalise some lemmas from unique factorisation domains to unique factorisation monoids, with the additional consequence that they no longer require addition to be defined.
Fill in TODOs for radical (radical a) = radical a and connecting UFM.primeFactors to Nat.primeFactors
Style changes The large-import is due to importing IsRadical for the definition of radical, and importing primality facts for natural numbers. The former is an obviously useful change to make, and the latter isn't necessary but the alternative is to have a separate file for radical on nat (which would be very short and a bit silly) or import RingTheory in Data/Nat, which would be undesirable. Upstreamed from the ABC-Exceptions project

Estimated changes

Modified Mathlib/Algebra/Divisibility/Units.lean

added theorem symmetric_isRelPrime

Modified Mathlib/NumberTheory/FLT/MasonStothers.lean

Modified Mathlib/NumberTheory/FLT/Polynomial.lean

Modified Mathlib/RingTheory/Polynomial/Radical.lean

Modified Mathlib/RingTheory/Radical.lean

modified theorem EuclideanDomain.divRadical_dvd_self

modified theorem EuclideanDomain.divRadical_isUnit

modified theorem EuclideanDomain.divRadical_mul

modified theorem EuclideanDomain.divRadical_mul_radical

modified theorem EuclideanDomain.divRadical_ne_zero

modified theorem EuclideanDomain.eq_divRadical

modified theorem EuclideanDomain.radical_mul_divRadical

added theorem IsRadical.dvd_radical

added theorem Nat.one_lt_radical_iff

added theorem Nat.radical_le_one_iff

added theorem Nat.radical_le_self_iff

added theorem Nat.radical_pos

added theorem Nat.two_le_radical_iff

modified theorem UniqueFactorizationDomain.disjoint_normalizedFactors

modified theorem UniqueFactorizationDomain.disjoint_primeFactors

modified theorem UniqueFactorizationDomain.mul_primeFactors_disjUnion

modified theorem UniqueFactorizationDomain.radical_mul

modified theorem UniqueFactorizationDomain.radical_neg

modified theorem UniqueFactorizationDomain.radical_neg_one

added theorem UniqueFactorizationMonoid.disjoint_primeFactors

added theorem UniqueFactorizationMonoid.dvd_radical_iff

added theorem UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible

added theorem UniqueFactorizationMonoid.isRadical_radical

added theorem UniqueFactorizationMonoid.mem_primeFactors

added theorem UniqueFactorizationMonoid.normalizedFactors_nodup

added theorem UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime

added theorem UniqueFactorizationMonoid.primeFactors_eq_empty_iff

added theorem UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors

added theorem UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion

added theorem UniqueFactorizationMonoid.primeFactors_mul_eq_union

added theorem UniqueFactorizationMonoid.primeFactors_of_isUnit

added theorem UniqueFactorizationMonoid.primeFactors_one

added theorem UniqueFactorizationMonoid.primeFactors_pow'

modified theorem UniqueFactorizationMonoid.primeFactors_pow

added theorem UniqueFactorizationMonoid.primeFactors_radical

added theorem UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactors

added theorem UniqueFactorizationMonoid.primeFactors_zero

added theorem UniqueFactorizationMonoid.radical_associated

added theorem UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset

added theorem UniqueFactorizationMonoid.radical_dvd_radical

added theorem UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors

added theorem UniqueFactorizationMonoid.radical_dvd_radical_iff_primeFactors_subset_primeFactors

modified theorem UniqueFactorizationMonoid.radical_dvd_self

modified theorem UniqueFactorizationMonoid.radical_eq_of_associated

added theorem UniqueFactorizationMonoid.radical_eq_of_primeFactors_eq

added theorem UniqueFactorizationMonoid.radical_eq_one_iff

added theorem UniqueFactorizationMonoid.radical_mul

added theorem UniqueFactorizationMonoid.radical_mul_dvd

modified theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left

modified theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_right

modified theorem UniqueFactorizationMonoid.radical_ne_zero

modified theorem UniqueFactorizationMonoid.radical_of_isUnit

modified theorem UniqueFactorizationMonoid.radical_of_prime

added theorem UniqueFactorizationMonoid.radical_one

deleted theorem UniqueFactorizationMonoid.radical_one_eq

modified theorem UniqueFactorizationMonoid.radical_pow

modified theorem UniqueFactorizationMonoid.radical_pow_of_prime

added theorem UniqueFactorizationMonoid.radical_prod

added theorem UniqueFactorizationMonoid.radical_prod_dvd

added theorem UniqueFactorizationMonoid.radical_radical

added theorem UniqueFactorizationMonoid.radical_zero

deleted theorem UniqueFactorizationMonoid.radical_zero_eq

added theorem UniqueFactorizationMonoid.squarefree_radical

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

added theorem UniqueFactorizationMonoid.disjoint_normalizedFactors

added theorem UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff

added theorem UniqueFactorizationMonoid.normalizedFactors_of_isUnit