toQuadraticForm' — Mathlib

English

If a matrix M is positive definite, then its associated quadratic form is positive definite.

Русский

Если матрица M положительно определена, то связанная с ней квадратичная форма положительно определена.

LaTeX

$$$$ M.PosDef \\Rightarrow M.toQuadraticMap'.PosDef. $$$$

Lean4

theorem toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) : M.toQuadraticMap'.PosDef :=
  by
  intro x hx
  simp only [Matrix.toQuadraticMap', LinearMap.BilinMap.toQuadraticMap_apply, toLinearMap₂'_apply']
  apply hM.2 x hx

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