toMatrix_compRight — Mathlib

English

The matrix of the right-composed bilinear form equals the bilinear matrix times the matrix of f.

Русский

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

LaTeX

$$BilinForm.toMatrix b (B.compRight f) = BilinForm.toMatrix b B * LinearMap.toMatrix b b f$$

Lean4

theorem toMatrix_compRight (B : BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁) :
    BilinForm.toMatrix b (B.compRight f) = BilinForm.toMatrix b B * LinearMap.toMatrix b b f :=
  LinearMap.toMatrix₂_compl₂ _ _ _ B _

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