Theorem IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg

Modification history

2026-03-20 18:13
Mathlib/Algebra/Module/SpanRankOperations.lean
feat(RingTheory): some lemma about span rank (#35337) …
Added IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fgView on Github →