posDef_toMatrix' — Mathlib

English

If a real quadratic form is positive definite, then its matrix representation is positive definite.

Русский

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

LaTeX

$$$$ Q.PosDef \\Rightarrow Q.toQuadraticMap'.PosDef. $$$$

Lean4

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

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