mul_toMatrix₂'_mul — Mathlib

English

The product of left and right matrices with a bilinear map corresponds to the bilinear map of the concatenated linear maps, i.e., aTranspose-left times B times c-right equals the composed bilinear form.

Русский

Произведение левой и правой матриц с билинейной формой соответствует билинейному отображению, получаемому от объединения линейных отображений.

LaTeX

$$$M \;*\; B \;*\; N = B^{\mathrm{compl}_{\!1\!2}}(M^T, N).$$$

Lean4

theorem mul_toMatrix₂'_mul (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :
    M * toMatrix₂' R B * N = toMatrix₂' R (B.compl₁₂ (toLin' Mᵀ) (toLin' N)) := by simp

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