Theorem LocalizedModule.subsingleton_iff

Modification history

2025-02-13 14:10

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

chore(RingTheory/IsLocalizedModule): extend API (#21483) …

Modified LocalizedModule.subsingleton_iff View 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 View on Github →