toLinAlgEquiv_self — Mathlib

English

With v1 as the basis, the matrix-to-linear-map equivalence applied to matrix M and the basis v1 reproduces the same action as M when expressed in the basis, i.e., Matrix.toLinAlgEquiv v1 M (v1 i) = ∑_j M_{j i} v1_j.

Русский

При базисе v1 эквивалентность матрица-линейное отображение действует так же, как сама матрица: Matrix.toLinAlgEquiv v1 M (v1 i) = ∑_j M_{j i} v1_j.

LaTeX

$$$\mathrm{toLinAlgEquiv}_{v_1} \, M\,(v_{1,i}) = \sum_j M_{j i} \; v_{1,j}$$$

Lean4

@[simp]
theorem toLinAlgEquiv_self (M : Matrix n n R) (i : n) : Matrix.toLinAlgEquiv v₁ M (v₁ i) = ∑ j, M j i • v₁ j :=
  Matrix.toLin_self _ _ _ _

Похожие утверждения