Commit 2024-07-19 09:45 23a781bb

View on Github →

chore (GroupTheory.MonoidLocalization): split file (#14877) We split GroupTheory.MonoidLocalization into Basic, Order, and MonoidWithZero.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/GroupTheory/MonoidLocalization.lean to Mathlib/GroupTheory/MonoidLocalization/Basic.lean

deleted theorem Localization.liftOn_zero

deleted def Localization.mkOrderEmbedding

deleted theorem Localization.mk_le_mk

deleted theorem Localization.mk_lt_mk

deleted theorem Localization.mk_zero

deleted theorem Submonoid.LocalizationMap.sec_zero_fst

deleted theorem Submonoid.LocalizationMap.subsingleton

deleted theorem Submonoid.LocalizationMap.toMap_injective_iff

deleted theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero

deleted theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular

deleted def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom

deleted structure Submonoid.LocalizationWithZeroMap

Created Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

added theorem Localization.liftOn_zero

added theorem Localization.mk_zero

added theorem Submonoid.LocalizationMap.sec_zero_fst

added theorem Submonoid.LocalizationMap.subsingleton

added theorem Submonoid.LocalizationMap.toMap_injective_iff

added theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero

added theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular

added def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom

added structure Submonoid.LocalizationWithZeroMap

Created Mathlib/GroupTheory/MonoidLocalization/Order.lean

added def Localization.mkOrderEmbedding

added theorem Localization.mk_le_mk

added theorem Localization.mk_lt_mk

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/Topology/Algebra/Localization.lean

Modified scripts/noshake.json

Modified scripts/style-exceptions.txt