toMatrix_apply — Mathlib

English

The matrix of B after multiplying on the left by M equals the transpose of M times the matrix of B, or equivalently, the matrix of the left-composed bilinear form.

Русский

Матрица B после левого умножения на M равна транспонированной M на матрицу B, иначе это матрица левой композиции билинейной формы.

LaTeX

$$M · toMatrix'(B) = toMatrix'(B.compLeft M^T)$$

Lean4

@[simp]
theorem toMatrix_apply (B : BilinForm R₁ M₁) (i j : n) : BilinForm.toMatrix b B i j = B (b i) (b j) :=
  LinearMap.toMatrix₂_apply _ _ B _ _

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