Commit 2024-10-15 06:49 dbbb99ab

View on Github →

chore(GroupTheory/MonoidLocalization/Basic): split off Away (#17731) This modifies GroupTheory/MonoidLocalization/Basic.lean by splitting off Localization.Away into its own file. This allows us to significantly reduce the imports, and in combination with #17730 we no longer need to know about rings or monoids with zero to define the localization of a monoid.

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/MonoidLocalization/Away.lean

added theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp

added theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq

added def Localization.Away.invSelf

added theorem Localization.Away.mk_eq_monoidOf_mk'

added theorem Submonoid.LocalizationMap.AwayMap.lift_comp

added theorem Submonoid.LocalizationMap.AwayMap.lift_eq

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

deleted theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp

deleted theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq

deleted def Localization.Away.invSelf

deleted theorem Localization.Away.mk_eq_monoidOf_mk'

deleted theorem Submonoid.LocalizationMap.AwayMap.lift_comp

deleted theorem Submonoid.LocalizationMap.AwayMap.lift_eq

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

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

Modified Mathlib/RingTheory/Localization/Ideal.lean

Modified Mathlib/SetTheory/Surreal/Dyadic.lean