Theorem Submonoid.LocalizationMap.subsingleton

Modification history

2025-12-05 10:18
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
chore(Algebra): extract `Submonoid.IsLocalizationMap` (#29596)
Modified Submonoid.LocalizationMap.subsingletonView on Github →
2025-08-22 15:03
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap (#27842) …
Modified Submonoid.LocalizationMap.subsingletonView on Github →
2024-08-30 08:52
Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
style: some formatting fixes (#16263) …
Modified Submonoid.LocalizationMap.subsingletonView on Github →
2024-07-19 09:45
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
chore (GroupTheory.MonoidLocalization): split file (#14877) …
Modified Submonoid.LocalizationMap.subsingletonView on Github →
2023-12-23 07:20
Mathlib/GroupTheory/MonoidLocalization.lean
feat: If the monoid S contains 0 then the localization at S is trivial (#9207)
Added Submonoid.LocalizationMap.subsingletonView on Github →