toBilin_basisFun — Mathlib

English

The matrix bilinear form obtained from Pi.basisFun equals the standard BilinForm.toMatrix representation.

Русский

Матрица билинейной формы, полученная из Pi.basisFun, равна стандартному представлению BilinForm.toMatrix.

LaTeX

$$BilinForm.toMatrix (Pi.basisFun R₁ n) = BilinForm.toMatrix'$$

Lean4

theorem toBilin_basisFun : Matrix.toBilin (Pi.basisFun R₁ n) = Matrix.toBilin' :=
  by
  ext M
  simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr, toBilin'_apply]

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