Theorem LinearIndependent.mulVec_surjective

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 LinearIndependent.mulVec_surjectiveView on Github →