Theorem Submodule.spanFinrank_of_not_fg

Modification history

2025-11-19 16:14
Mathlib/Algebra/Module/SpanRank.lean
feat: power series over a noetherian ring is noetherian (#31149) …
Added Submodule.spanFinrank_of_not_fgView on Github →