Theorem Submodule.lift_spanRank_le_iff_exists_span_set_card_le

Modification history

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