toMatrix₂'_comp — Mathlib

English

The composition of bilinear maps with respect to l and r corresponds to a product of matrices with transposed left factor and right factor, matching the bilinear composition via compl₁₂.

Русский

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

LaTeX

$$$\mathrm{toMatrix}_{2}' R (B\circ_{l,r}) = (\mathrm{toMatrix}' l)^T \; \mathrm{toMatrix}_{2}' R B \; (\mathrm{toMatrix}' r).$$$

Lean4

theorem toMatrix₂'_comp (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (n' → R) →ₗ[R] n → R) :
    toMatrix₂' R (B.comp f) = (toMatrix' f)ᵀ * toMatrix₂' R B :=
  by
  rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂]
  simp

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