toMatrix'_compRight — Mathlib

English

If B is a bilinear form and f is a linear map, then the matrix after right-composition with f equals B's matrix times f's matrix.

Русский

Если B — билинейная форма и f — линейное отображение, то матрица после правой композиции равна матрице B, умноженной на матрицу f.

LaTeX

$$$\operatorname{toMatrix'}\big(B \circRight f\big) = \operatorname{toMatrix'}(B) \; f$$$

Lean4

theorem toMatrix'_compRight (B : BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁) :
    (B.compRight f).toMatrix' = B.toMatrix' * f.toMatrix' :=
  B.toMatrix₂'_compl₂ _

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