Theorem Module.nonempty_support_of_nontrivial

Modification history

2025-11-10 13:35
Mathlib/RingTheory/Support.lean
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) …
Added Module.nonempty_support_of_nontrivialView on Github →