Theorem linearIndependent_of_top_le_span_of_card_le_finrank

Modification history

2025-12-08 23:04
Mathlib/LinearAlgebra/Dimension/OrzechProperty.lean
chore(LinearAlgebra/Dimension): generalize and golf (#32339) …
Added linearIndependent_of_top_le_span_of_card_le_finrankView on Github →