Theorem LocalizedModule.exists_subsingleton_away

Modification history

2025-03-26 11:53
Mathlib/RingTheory/Support.lean
feat(RingTheory): support of quotient module (#20292)
Modified LocalizedModule.exists_subsingleton_awayView on Github →
2024-07-22 15:39
Mathlib/RingTheory/Support.lean
feat(RingTheory/Support): Define support of a module (#14507) …
Added LocalizedModule.exists_subsingleton_awayView on Github →