toLinearMap₂'_comp — Mathlib

English

The composition with a bilinear map on the right is given by a matrix product with the transposed left factor; the identity matches the previous corollaries about compl₂ and the matrix product.

Русский

Композиция справа выражается через произведение матриц с транспонированным левым множителем; тождество согласуется с предыдущими следствиями о compl₂ и произведении матриц.

LaTeX

$$$B.{\mathrm{compl}_{2}}(P, Q) = \mathrm{toMatrix}_{2}'(R) B \cdot (P^T) \cdot Q.$$$

Lean4

theorem toLinearMap₂'_comp (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
    LinearMap.compl₁₂ (Matrix.toLinearMap₂' R M) (toLin' P) (toLin' Q) = toLinearMap₂' R (Pᵀ * M * Q) :=
  (LinearMap.toMatrix₂' R).injective (by simp)

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