toMatrixAlgEquiv_apply — Mathlib

English

For a basis v1 and a linear map f: M1→M1, the (i,j)-entry of the matrix representing f with respect to v1 is the i-th coordinate of f(v1 j) in the basis v1.

Русский

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

LaTeX

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

Lean4

theorem toMatrixAlgEquiv_apply (f : M₁ →ₗ[R] M₁) (i j : n) :
    LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i := by
  simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply]

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