toBilin'_comp — Mathlib

English

The bilinear form associated to the product of matrices is the bilinear form of the composition of the corresponding maps.

Русский

Билинейная форма, связанная с произведением матриц, равна билинейной форме композиции соответствующих отображений.

LaTeX

$$$M^{\!}\toBilin' (P^{\top} M Q) = (P^{\top} M Q)^{\ldots}$$$

Lean4

theorem toBilin'_comp (M : Matrix n n R₁) (P Q : Matrix n o R₁) :
    M.toBilin'.comp P.toLin' Q.toLin' = (Pᵀ * M * Q).toBilin' :=
  BilinForm.toMatrix'.injective
    (by simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin'])

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