toMatrix₂_compl₂ — Mathlib

English

For a bilinear map B and a right insertion f, the matrix of the compl₂ operation relates to the original matrix B by multiplying with the matrix of f on the right.

Русский

Для билинейного отображения B и правой вставки f матрица операции compl₂ связывает исходную матрицу B через умножение справа на матрицу f.

LaTeX

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

Lean4

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

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