toMatrix'_apply — Mathlib

English

For a bilinear form B on (n→R), the i,j entry of its matrix representation is B evaluated at the i-th and j-th standard basis vectors.

Русский

Для билинейной формы B на (n→R) элемент матрицы в позиции (i,j) равен B(e_i,e_j), где e_i — i-ая стандартная базисная вектора.

LaTeX

$$$(\mathrm{toMatrix'} B)_{ij} = B(e_i,e_j)$$$

Lean4

@[simp]
theorem toMatrix'_apply (B : BilinForm R₁ (n → R₁)) (i j : n) :
    BilinForm.toMatrix' B i j = B (Pi.single i 1) (Pi.single j 1) :=
  LinearMap.toMatrix₂'_apply _ _ _

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