mul_toMatrix'_mul — Mathlib

English

For a bilinear form B and matrices M,N, the matrix representing the bilinear form composed with left and right linear maps equals M^T times B times N.

Русский

Для билинейной формы B и матриц M,N, матрица, представляющая композицию билинейной формы с левым и правым отображениями, равна M^T B N.

LaTeX

$$$M \cdot B_{\text{toMatrix}} \cdot N = (B \circ (M^{\top})^{\!\!} \circ N)_{\text{toMatrix}}$$$

Lean4

theorem mul_toMatrix'_mul (B : BilinForm R₁ (n → R₁)) (M : Matrix o n R₁) (N : Matrix n o R₁) :
    M * B.toMatrix' * N = (B.comp (Mᵀ).toLin' N.toLin').toMatrix' :=
  B.mul_toMatrix₂'_mul _ _

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