toMatrix'_mul — Mathlib

English

Multiplication of a matrix with a bilinear-form matrix corresponds to the bilinear form applied to a left-transpose composition.

Русский

Умножение матрицы на матрицу билинейной формы соответствует применению билинейной формы к левой транспозиции композиции.

LaTeX

$$$B \toMatrix' \cdot M = (B.compRight (Matrix.toLin' M)).toMatrix'$$$

Lean4

theorem toMatrix'_mul (B : BilinForm R₁ (n → R₁)) (M : Matrix n n R₁) :
    BilinForm.toMatrix' B * M = BilinForm.toMatrix' (B.compRight (Matrix.toLin' M)) :=
  B.toMatrix₂'_mul _

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