Theorem LocalizedModule.subsingleton

Modification history

2023-12-23 07:20

Mathlib/Algebra/Module/LocalizedModule.lean

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

Added LocalizedModule.subsingleton View on Github →