English
An element a is strictly positive if and only if sqrt(a) is strictly positive and a = sqrt(a) sqrt(a).
Русский
Элемент a строго положителен тогда и только тогда, когда sqrt(a) строгоположителен и a = sqrt(a) sqrt(a).
LaTeX
$$$\text{IsStrictlyPositive}(a) \iff \bigl(\text{IsStrictlyPositive}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a}\bigr)$$$
Lean4
theorem _root_.CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt {a : A} :
IsStrictlyPositive a ↔ IsUnit (sqrt a) ∧ a = sqrt a * sqrt a :=
CStarAlgebra.isStrictlyPositive_TFAE.out 0 2
