toMatrix_compLeft — Mathlib

English

The matrix of the left-composed bilinear form equals the transpose of the matrix of f multiplied by the matrix of B.

Русский

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

LaTeX

$$BilinForm.toMatrix b (B.compLeft f) = (LinearMap.toMatrix b b f)^T * BilinForm.toMatrix b B$$

Lean4

theorem toMatrix_compLeft (B : BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁) :
    BilinForm.toMatrix b (B.compLeft f) = (LinearMap.toMatrix b b f)ᵀ * BilinForm.toMatrix b B :=
  LinearMap.toMatrix₂_comp _ _ _ B _

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