Commit 2025-08-24 13:04 8b7d3d33

View on Github →

chore(Algebra): generalize results on IsLocalization to Submonoid.LocalizationMap (#27862) Also adds some lemmas connecting IsRegular to nonZeroDivisors, and IsCancelMulZero to NoZeroDivisors.

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

modified theorem Submonoid.LocalizationMap.isCancelMul

modified theorem Submonoid.LocalizationMap.map_isRegular

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

added theorem Submonoid.LocalizationMap.map_eq_zero_iff

added theorem Submonoid.LocalizationMap.map_nonZeroDivisors_le

added theorem Submonoid.LocalizationMap.mk'_eq_zero_iff

added theorem Submonoid.LocalizationMap.mk'_zero

added theorem Submonoid.LocalizationMap.noZeroDivisors

added theorem Submonoid.LocalizationMap.nonZeroDivisors_le_comap

added theorem Submonoid.LocalizationMap.nontrivial

added theorem Submonoid.LocalizationMap.subsingleton_iff

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

modified theorem IsLocalization.isDomain_localization

modified theorem IsLocalization.isDomain_of_le_nonZeroDivisors

modified theorem IsLocalization.map_eq_zero_iff

modified theorem IsLocalization.mk'_eq_zero_iff

modified theorem IsLocalization.mk'_zero

modified theorem IsLocalization.noZeroDivisors

Modified Mathlib/RingTheory/Localization/Ideal.lean

Modified Mathlib/RingTheory/Trace/Quotient.lean