toMatrix'_comp — Mathlib

English

If B is a bilinear form on (n→R) and l,r are linear maps from (o→R) to (n→R), then the matrix of the composed form B ∘ (l,r) is the product l^T B r.

Русский

Если B — билинейная форма на (n→R), и l,r — линейные отображения из (o→R) в (n→R), то матрица композиции B ∘ (l,r) равна произведению l^T B r.

LaTeX

$$$\operatorname{toMatrix'}\big(B \circ (l,r)\big) = l^{\top} \operatorname{toMatrix'}(B) \; r$$$

Lean4

@[simp]
theorem toMatrix'_comp (B : BilinForm R₁ (n → R₁)) (l r : (o → R₁) →ₗ[R₁] n → R₁) :
    (B.comp l r).toMatrix' = l.toMatrix'ᵀ * B.toMatrix' * r.toMatrix' :=
  B.toMatrix₂'_compl₁₂ _ _

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