Commit 2025-11-09 18:25 58465418
View on Github →feat(RingTheory): improve radical_eq_of_primeFactors_eq (#31435)
The radicals of two elements are equal if and only if their sets of prime factors coincide.
Moves:
- UniqueFactorizationMonoid.radical_eq_of_primeFactors_eq -> UniqueFactorizationMonoid.radical_eq_iff_primeFactors_eq