Theorem LocalizedModule.subsingleton_iff_ker_eq_top

Modification history

2025-02-13 14:10
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
chore(RingTheory/IsLocalizedModule): extend API (#21483) …
Modified LocalizedModule.subsingleton_iff_ker_eq_topView on Github →
2024-07-22 15:39
Mathlib/Algebra/Module/LocalizedModule.lean
feat(RingTheory/Support): Define support of a module (#14507) …
Added LocalizedModule.subsingleton_iff_ker_eq_topView on Github →