Theorem Submodule.spanFinrank_map_le_of_fg

Modification history

2026-02-02 08:04
Mathlib/Algebra/Module/SpanRank.lean
feat(Algebra/Module/SpanRank): add comparing lemmas for span rank (#33359)
Modified Submodule.spanFinrank_map_le_of_fgView on Github →
2025-11-19 16:14
Mathlib/Algebra/Module/SpanRank.lean
feat: power series over a noetherian ring is noetherian (#31149) …
Added Submodule.spanFinrank_map_le_of_fgView on Github →