toMatrixAux_apply — Mathlib

English

The matrices representing a linear map f with respect to different bases compose to give the matrix of f with the corresponding domain and codomain bases.

Русский

Матрицы линейного отображения f в разных базисах компонуются и дают матрицу f с соответствующими базисами области и кода.

LaTeX

$$$\text{basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix}$$$

Lean4

@[simp]
theorem toMatrixAux_apply (B : BilinForm R₁ M₁) (b : n → M₁) (i j : n) :
    BilinForm.toMatrixAux b B i j = B (b i) (b j) :=
  LinearMap.toMatrix₂Aux_apply R₁ B _ _ _ _

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