English
For a matrix M, vecMul is injective if and only if the rows of M are linearly independent.
Русский
Для матрицы M отображение vecMul инъективно тогда и только тогда, когда строки M линейно независимы.
LaTeX
$$Function.Injective M.vecMul ↔ LinearIndependent R M.row$$
Lean4
theorem vecMul_injective_iff {M : Matrix m n R} : Function.Injective M.vecMul ↔ LinearIndependent R M.row :=
by
rw [← coe_vecMulLinear, linearIndependent_iff_injective_fintypeLinearCombination]
congr! 1
exact funext fun _ => Matrix.vecMul_eq_sum _ _