Commit 2024-10-17 19:04 e759b3b1

View on Github →

feat: UniqueFactorizationMonoid.factors_rel_of_associated (#17260)

Estimated changes

Modified Mathlib/RingTheory/Radical.lean

added theorem Associated.primeFactors_eq

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

added theorem Associated.normalizedFactors_eq

added theorem UniqueFactorizationMonoid.factors_rel_of_associated