toMatrix_comp — Mathlib

English

The matrix of the composed bilinear form B with l and r equals the product l^T B r using bases b and c.

Русский

Матрица композиции билинейной формы B с l и r равна произведению l^T B r, когда заданы базы b и c.

LaTeX

$$BilinForm.toMatrix c (B.comp l r) = (LinearMap.toMatrix c b l)^T * BilinForm.toMatrix b B * LinearMap.toMatrix c b r$$

Lean4

theorem toMatrix_comp (B : BilinForm R₁ M₁) (l r : M₂' →ₗ[R₁] M₁) :
    BilinForm.toMatrix c (B.comp l r) =
      (LinearMap.toMatrix c b l)ᵀ * BilinForm.toMatrix b B * LinearMap.toMatrix c b r :=
  LinearMap.toMatrix₂_compl₁₂ _ _ _ _ B _ _

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