2025-05-22 12:54
Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
feat(UniqueFactorizationMonoid): a `MulEquiv` that commutes with `normalize` preserves `normalizedFactors` (#25080)
Added UniqueFactorizationMonoid.normalizedFactorsEquiv