posSemidef_sqrt — Mathlib

English

If A is positive semidefinite, then its square root is well-defined and itself positive semidefinite; in particular, the square root is Hermitian.

Русский

Если A положительно полуопределена, то её квадратный корень существует и сам является положительно полуопределённой и эрмитовым.

LaTeX

$$$\text{PosSemidef}(\sqrt{A}).$$$

Lean4

@[deprecated CFC.sqrt_nonneg (since := "2025-09-22")]
theorem posSemidef_sqrt : PosSemidef (CFC.sqrt A) :=
  CFC.sqrt_nonneg A |>.posSemidef

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