Commit 2026-10-01 09:26 bc9cec55

feat(LinearAlgebra/Matrix/Rank): linearly independent rows give a surjective mulVec (#43956) LinearIndependent.rank_matrix says a matrix with linearly independent rows has full row rank. This PR adds surjectivity consequences for mulVec/vecMul, plus rank characterizations:

• LinearIndependent.mulVec_surjective: over a semisimple ring, linearly independent rows give surjective mulVec (reviewer-supplied proof: vecMul injective → left inverse via IsSemisimpleModule.extension_property → right inverse for M). No finiteness hypothesis on the row index m; Finite m follows from linear independence. Fintype n comes from the file's variables, as mulVec requires.
• LinearIndependent.vecMul_surjective: over a commutative semisimple ring, linearly independent columns give surjective vecMul, by transposition from the row version.
• Matrix.mulVec_surjective_iff_rank_eq_card and Matrix.vecMul_surjective_iff_rank_eq_card: over a field, surjectivity iff full row/column rank.