toMatrix₂_apply — Mathlib

English

The entry in the i-th row and j-th column of the matrix representing a bilinear map B with respect to bases b1,b2 is exactly B(b1_i, b2_j).

Русский

Элемент матрицы, соответствующий би-отображению B в базисах b1,b2, равен B(b1_i, b2_j).

LaTeX

$$$\mathrm{toMatrix}_{\mathrm{sl}2}'(R)\ B\, i,j = B\bigl(\!\Pi_i(1)\bigr),\bigl(\Pi_j(1)\bigr).$$$

Lean4

@[simp]
theorem toMatrix₂_apply (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) (i : n) (j : m) :
    LinearMap.toMatrix₂ b₁ b₂ B i j = B (b₁ i) (b₂ j) := by
  simp only [toMatrix₂, LinearEquiv.trans_apply, toMatrix₂'_apply, LinearEquiv.arrowCongr_apply,
    Basis.equivFun_symm_apply, Pi.single_apply, ite_smul, one_smul, zero_smul, sum_ite_eq', mem_univ, ↓reduceIte,
    LinearEquiv.refl_apply]

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