Commit 2025-08-22 15:03 07d0b33f

View on Github →

chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap (#27842) because every Submonoid.LocalizationMap automatically preserves zero. Also removes a condition from isLeftRegular_of_le_isCancelMulZero by proving map_isRegular, which is used to prove other related lemmas. toMap_injective_iff is moved from MonoidWithZero.lean to Basic.lean.

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

added theorem Submonoid.LocalizationMap.injective_iff

added theorem Submonoid.LocalizationMap.isCancelMul

added theorem Submonoid.LocalizationMap.map_isRegular

added theorem Submonoid.LocalizationMap.top_injective_iff

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

deleted theorem Submonoid.LocalizationMap.injective_iff

added theorem Submonoid.LocalizationMap.isCancelMulZero

added theorem Submonoid.LocalizationMap.lift₀_apply

added theorem Submonoid.LocalizationMap.lift₀_def

modified theorem Submonoid.LocalizationMap.subsingleton

added def Submonoid.LocalizationMap.toMonoidWithZeroHom

deleted theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero

deleted theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular

deleted theorem Submonoid.LocalizationWithZeroMap.lift_apply

deleted theorem Submonoid.LocalizationWithZeroMap.lift_def

deleted def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom

deleted structure Submonoid.LocalizationWithZeroMap

Modified Mathlib/RingTheory/Localization/Defs.lean

deleted def IsLocalization.toLocalizationWithZeroMap

Modified Mathlib/RingTheory/OrderOfVanishing.lean