English
An element a is strictly positive if and only if there exists b strictly positive with a = b b.
Русский
Элемент a строго положителен тогда и только тогда, когда существует строго положительный b, такой что a = b b.
LaTeX
$$$\text{IsStrictlyPositive}(a) \iff \exists b\, (\text{IsStrictlyPositive}(b) \land a = b \cdot b)$$$
Lean4
theorem _root_.CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self {a : A} :
IsStrictlyPositive a ↔ ∃ b, IsStrictlyPositive b ∧ a = b * b :=
CStarAlgebra.isStrictlyPositive_TFAE.out 0 3
