Commit 2025-08-13 18:44 f7674787

View on Github →

refactor: make use of FunLike for Submonoid.LocalizationMap (#22655) From Toric

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization/Away.lean

modified theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp

modified theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq

modified theorem Submonoid.LocalizationMap.AwayMap.lift_comp

modified theorem Submonoid.LocalizationMap.AwayMap.lift_eq

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

modified theorem Localization.mk_one_eq_monoidOf_mk

modified theorem Localization.mulEquivOfQuotient_monoidOf

modified theorem Localization.mulEquivOfQuotient_symm_monoidOf

modified theorem Submonoid.LocalizationMap.epic_of_localizationMap

modified theorem Submonoid.LocalizationMap.eq_iff_eq

modified theorem Submonoid.LocalizationMap.eq_mk'_iff_mul_eq

modified theorem Submonoid.LocalizationMap.eq_of_eq

modified theorem Submonoid.LocalizationMap.ext

modified theorem Submonoid.LocalizationMap.isUnit_comp

modified theorem Submonoid.LocalizationMap.lift_comp

modified theorem Submonoid.LocalizationMap.lift_eq

modified theorem Submonoid.LocalizationMap.lift_unique

modified theorem Submonoid.LocalizationMap.map_comp

modified theorem Submonoid.LocalizationMap.map_eq

modified theorem Submonoid.LocalizationMap.map_left_cancel

modified theorem Submonoid.LocalizationMap.map_mul_left

modified theorem Submonoid.LocalizationMap.map_mul_right

modified theorem Submonoid.LocalizationMap.map_right_cancel

modified theorem Submonoid.LocalizationMap.map_spec

modified theorem Submonoid.LocalizationMap.map_units

modified theorem Submonoid.LocalizationMap.mk'_eq_iff_eq_mul

modified theorem Submonoid.LocalizationMap.mk'_mul

modified theorem Submonoid.LocalizationMap.mk'_mul_cancel_left

modified theorem Submonoid.LocalizationMap.mk'_mul_cancel_right

modified theorem Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul

modified theorem Submonoid.LocalizationMap.mk'_one

modified theorem Submonoid.LocalizationMap.mk'_spec'

modified theorem Submonoid.LocalizationMap.mk'_spec

modified theorem Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul

modified theorem Submonoid.LocalizationMap.mul_mk'_one_eq_mk'

modified theorem Submonoid.LocalizationMap.surj

deleted theorem Submonoid.LocalizationMap.toMap_injective

added theorem Submonoid.LocalizationMap.toMonoidHom_apply

added theorem Submonoid.LocalizationMap.toMonoidHom_injective

Modified Mathlib/GroupTheory/MonoidLocalization/DivPairs.lean

modified def Submonoid.divPairs

modified theorem Submonoid.mem_divPairs

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

added theorem Submonoid.LocalizationMap.injective_iff

modified theorem Submonoid.LocalizationMap.sec_zero_fst

deleted theorem Submonoid.LocalizationMap.toMap_injective_iff

Modified Mathlib/RingTheory/Localization/Defs.lean

added theorem IsLocalization.coe_toLocalizationMap

added theorem IsLocalization.toLocalizationMap_apply

deleted theorem IsLocalization.toLocalizationMap_toMap

deleted theorem IsLocalization.toLocalizationMap_toMap_apply

added theorem IsLocalization.toLocalizationMap_toMonoidHom

modified theorem Localization.monoidOf_eq_algebraMap

Modified Mathlib/RingTheory/Valuation/ExtendToLocalization.lean