toMatrix₂'_compl₂ — Mathlib

English

Multiplication of matrices corresponds to concatenating bilinear forms, i.e., composing the associated bilinear forms yields the product of matrices with a suitable transposition convention.

Русский

Умножение матриц соответствует объединению билинейных форм, т.е. композиция соответствующих билинейных форм даёт произведение матриц с подходящей транспозицией.

LaTeX

$$$M\, B \;=\; B\,\!\circ \;M \;\approx\; \mathrm{toMatrix}_{2}'(R) (B) \;\text{and}\; M * B = \mathrm{toMatrix}_{2}'(R) (B)$.$$

Lean4

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

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