toMatrix₂'_mul — Mathlib

English

Multiplying a bilinear map by a matrix on the left or right corresponds to composing with the corresponding linear maps on the left or right, via compl₁₂; this preserves the bilinear structure.

Русский

Умножение билинейного отображения слева или справа на матрицу соответствует композиции с соответствующими линейными отображениями; сохраняется билинейность.

LaTeX

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

Lean4

theorem toMatrix₂'_mul (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix m m' R) :
    toMatrix₂' R B * M = toMatrix₂' R (B.compl₂ <| toLin' M) := by simp only [B.toMatrix₂'_compl₂, toMatrix'_toLin']

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