Commit 2023-12-23 07:20 66c1128b

View on Github →

feat: If the monoid S contains 0 then the localization at S is trivial (#9207)

Estimated changes

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem LocalizedModule.subsingleton

Modified Mathlib/GroupTheory/MonoidLocalization.lean

added theorem Submonoid.LocalizationMap.subsingleton

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.subsingleton