English
In the same setting, the nine equivalent conditions for strict positivity hold as a TF AE statement.
Русский
В той же настройке девять эквивалентных условий строгой положительности образуют цепочку эквивалентностей.
LaTeX
$$$\text{IsStrictlyPositive}(a) \iff \text{IsStrictlyPositive}(\sqrt{a}) \land a = \sqrt{a} \cdot \sqrt{a} \iff \cdots \iff \text{IsSelfAdjoint}(a) \land \forall x \in \operatorname{spectrum}_{\mathbb{R}}(a), 0 < x$$$
Lean4
theorem _root_.CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self {a : A} :
IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b :=
CStarAlgebra.isStrictlyPositive_TFAE.out 0 4
