Commit 2026-02-02 08:04 f6d9e1de

View on Github →

feat(Algebra/Module/SpanRank): add comparing lemmas for span rank (#33359)

Estimated changes

Modified Mathlib/Algebra/Module/SpanRank.lean

added theorem Submodule.le_spanRank_restrictScalars

modified theorem Submodule.spanFinrank_map_le_of_fg

added theorem Submodule.spanRank_eq_of_equiv

added theorem Submodule.spanRank_map_eq_of_injective

modified theorem Submodule.spanRank_map_le

added theorem Submodule.spanRank_range_le

added theorem Submodule.spanRank_restrictScalars_eq

added theorem Submodule.spanRank_top