toMatrix'_compLeft — Mathlib

English

If B is a bilinear form and f is a linear map on the same space, then the matrix of B after left-composition with f is f^T times the matrix of B.

Русский

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

LaTeX

$$$\operatorname{toMatrix'}\big(B \circLeft f\big) = f^{\top} \operatorname{toMatrix'}(B)$$$

Lean4

theorem toMatrix'_compLeft (B : BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁) :
    (B.compLeft f).toMatrix' = f.toMatrix'ᵀ * B.toMatrix' :=
  B.toMatrix₂'_comp _

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