posDef_of_toMatrix' — Mathlib

English

If the matrix associated to a real quadratic form is positive definite, then the quadratic form is positive definite.

Русский

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

LaTeX

$$$$ M^{\\text{IsSymm}} \\land M.toQuadraticMap'.PosDef \\Rightarrow M.PosDef. $$$$

Lean4

theorem posDef_of_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Q.toMatrix'.PosDef) : Q.PosDef :=
  by
  rw [← toQuadraticMap_associated ℝ Q, ← (LinearMap.toMatrix₂' ℝ).left_inv ((associatedHom (R := ℝ) ℝ) Q)]
  exact hQ.toQuadraticForm'

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