Commit 2024-08-16 13:44 b899e710

View on Github →

refactor: Restrict scope of radical to UniqueFactorizationDomain (#15826) Restrict scope of radical as suggested in this comment by @YaelDillies.

Estimated changes

Modified Mathlib/RingTheory/Radical.lean

added def UniqueFactorizationMonoid.primeFactors

added theorem UniqueFactorizationMonoid.primeFactors_pow

added def UniqueFactorizationMonoid.radical

added theorem UniqueFactorizationMonoid.radical_dvd_self

added theorem UniqueFactorizationMonoid.radical_eq_of_associated

added theorem UniqueFactorizationMonoid.radical_mul_unit

added theorem UniqueFactorizationMonoid.radical_of_prime

added theorem UniqueFactorizationMonoid.radical_one_eq

added theorem UniqueFactorizationMonoid.radical_pow

added theorem UniqueFactorizationMonoid.radical_pow_of_prime

added theorem UniqueFactorizationMonoid.radical_unit_eq_one

added theorem UniqueFactorizationMonoid.radical_unit_mul

added theorem UniqueFactorizationMonoid.radical_zero_eq

deleted def primeFactors

deleted theorem primeFactors_pow

deleted def radical

deleted theorem radical_dvd_self

deleted theorem radical_eq_of_associated

deleted theorem radical_mul_unit

deleted theorem radical_of_prime

deleted theorem radical_one_eq

deleted theorem radical_pow

deleted theorem radical_pow_of_prime

deleted theorem radical_unit_eq_one

deleted theorem radical_unit_mul

deleted theorem radical_zero_eq