English
Let M be an m×n matrix and i an index from n. The map Matrix.toLin applied to the i-th basis vector v1 i yields a linear combination of the v2-basis: Matrix.toLin v1 v2 M (v1 i) = ∑_j M_{j i} · v2_j.
Русский
Пусть M — матрица размера m×n, и i — индекс из {1,…,n}. Применение линейного отображения Matrix.toLin к вектору v1_i даёт линейную комбинацию базовых векторов v2_j: Matrix.toLin v1 v2 M (v1 i) = ∑_j M_{j i} · v2_j.
LaTeX
$$$\mathrm{toLin}_{v_1,v_2}(M)(v_{1,i}) = \sum_j M_{j i} \; v_{2,j}$$$
Lean4
@[simp]
theorem toLin_self (M : Matrix m n R) (i : n) : Matrix.toLin v₁ v₂ M (v₁ i) = ∑ j, M j i • v₂ j :=
by
rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]
rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same, mul_one]
· intro i' _ i'_ne
rw [Finsupp.single_eq_of_ne i'_ne, mul_zero]
· intros
have := Finset.mem_univ i
contradiction
