posDef_sqrt — Mathlib

English

If M is positive definite, then its square root is positive definite.

Русский

Если M положительно определена, то её квадратный корень положительно определён.

LaTeX

$$$M^{PosDef} \Rightarrow (\sqrt{M})^{PosDef}$$$

Lean4

theorem posDef_sqrt [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : PosDef (CFC.sqrt M) :=
  (CFC.sqrt_nonneg M).posSemidef.posDef_iff_isUnit.mpr <| CFC.isUnit_sqrt_iff M hM.posSemidef.nonneg |>.mpr hM.isUnit

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