Theorem Submodule.Quotient.nontrivial_of_ne_top

Modification history

2025-11-10 13:35
Mathlib/LinearAlgebra/Quotient/Basic.lean
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) …
Added Submodule.Quotient.nontrivial_of_ne_topView on Github →