Commit 2026-07-13 10:57 a7a08642

View on Github →

feat(Algebra): localization preserves unique factorization (#33832)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

added theorem IsUnit.multisetProd_iff

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

added theorem Associated.acc_dvdNotUnit_iff

added theorem Associated.dvdNotUnit_left

added theorem Associated.dvdNotUnit_left_iff

added theorem Associated.dvdNotUnit_right_iff

modified theorem dvdNotUnit_of_dvdNotUnit_associated

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Created Mathlib/GroupTheory/MonoidLocalization/Divisibility.lean

Created Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean

added theorem Submonoid.LocalizationMap.eq_isUnit_map_mul_irreducible_of_irreducible_map

added theorem Submonoid.LocalizationMap.map_prime

added theorem Submonoid.LocalizationMap.uniqueFactorizationMonoid

added theorem UniqueFactorizationMonoid.of_isLocalization

Modified Mathlib/RingTheory/Ideal/UFD.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

modified theorem IsLocalization.algebraMap_isUnit_iff

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Localization.lean

deleted theorem UniqueFactorizationMonoid.of_isLocalization