Theorem Matrix.mulVec_surjective_iff_rank_eq_card

Modification history

2026-10-01 09:26
Mathlib/LinearAlgebra/Matrix/Rank.lean
feat(LinearAlgebra/Matrix/Rank): linearly independent rows give a surjective mulVec (#43956) …
Added Matrix.mulVec_surjective_iff_rank_eq_cardView on Github →