toMatrix₂_comp — Mathlib

English

If B is bilinear and f is a linear map, the matrix of the composed map B ∘ f equals the product of the matrix of f (transposed) with the matrix of B.

Русский

Если B — билинейное отображение, а f — линейное, то матрица композиции B ∘ f равна произведению транспонированной матрицы f на матрицу B.

LaTeX

$$$$ \mathrm{toMatrix}_2^{b_1',b_2}\bigl(B \circ f\bigr) = \bigl(\mathrm{toMatrix}_{b_1',b_1} f\bigr)^{\top} \; \mathrm{toMatrix}_2^{b_1,b_2}(B). $$$$

Lean4

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

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