Commit 2025-05-22 12:54 cfc4bc01

View on Github →

feat(UniqueFactorizationMonoid): a MulEquiv that commutes with normalize preserves normalizedFactors (#25080)

Estimated changes

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

added theorem normalize_eq_normalize_iff_associated

Modified Mathlib/Algebra/Ring/Divisibility/Basic.lean

added theorem map_dvd_iff_dvd_symm

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

added theorem UniqueFactorizationMonoid.dvd_of_normalized_factor

added theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff'

added def UniqueFactorizationMonoid.normalizedFactorsEquiv

added theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_apply

added theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply