toMatrix'_comp — Mathlib

English

The matrix of a composition Q ∘ f is given by a product involving the transpose of the matrix of f and Q’s matrix.

Русский

Матрица композиции Q ∘ f задаётся произведением, в котором участвуют транспонированная матрица f и матрица Q.

LaTeX

$$(Q.comp f).toMatrix' = (LinearMap.toMatrix' f)^{\top} * Q.toMatrix' * (LinearMap.toMatrix' f)$$

Lean4

@[simp]
theorem toMatrix'_comp (Q : QuadraticMap R (m → R) R) (f : (n → R) →ₗ[R] m → R) :
    (Q.comp f).toMatrix' = (LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * (LinearMap.toMatrix' f) := by
  simp only [QuadraticMap.associated_comp, LinearMap.toMatrix₂'_compl₁₂, toMatrix']

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