mul_toMatrix' — Mathlib

English

The product of M with a matrix-represented bilinear map equals the matrix of the bilinear map composed with the left/right transposes; the statement matches the functorial behavior of toMatrix₂'.

Русский

Произведение M на матрично представляемое билинейное отображение равно матрице билинейного отображения, композиция с левой/правой транспонированием сохраняется.

LaTeX

$$$M \cdot \mathrm{toMatrix}_{2}'(R) B = \mathrm{toMatrix}_{2}'(R) (B \circ (M^T, \mathrm{Id})).$$$

Lean4

theorem mul_toMatrix' (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R) :
    M * toMatrix₂' R B = toMatrix₂' R (B.comp <| toLin' Mᵀ) := by
  simp only [B.toMatrix₂'_comp, transpose_transpose, toMatrix'_toLin']

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