toMatrixAlgEquiv_id — Mathlib

English

For a basis v1 and a linear map f: M1→M1, the (i,j)-entry of the matrix representing f equals the i-th coordinate of f(v1_j) when expressed in the basis v1.

Русский

Для базиса v1 и линейного отображения f определить элемент (i,j) матрицы, представляющей f, как i-ю координату f(v1_j) в базисе v1.

LaTeX

$$$\mathrm{toMatrixAlgEquiv}_{v_1} f\, i j = v_1.repr (f(v_1 j))_i$$$

Lean4

theorem toMatrixAlgEquiv_id : LinearMap.toMatrixAlgEquiv v₁ id = 1 := by
  simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]

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