Theorem IsLocalization.subsingleton

Modification history

2024-10-15 07:35
Mathlib/RingTheory/Localization/Basic.lean
chore(RingTheory/Localization/Basic): split off `Defs` (#17735) …
Modified IsLocalization.subsingletonView on Github →
2023-12-23 07:20
Mathlib/RingTheory/Localization/Basic.lean
feat: If the monoid S contains 0 then the localization at S is trivial (#9207)
Added IsLocalization.subsingletonView on Github →