isStrictlyPositive_iff_eq_star_mul_self

English

An element a is strictly positive if and only if there exists b unit with a = b * star(b).

Русский

Элемент a строго положителен тогда и только тогда, когда существует модуль b такой, что a = b * star(b).

LaTeX

$$$\text{IsStrictlyPositive}(a) \iff \exists b, \text{IsUnit}(b) \land a = b \cdot \star b$$$

Lean4

theorem _root_.CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self {a : A} :
    IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ a = star b * b :=
  CStarAlgebra.isStrictlyPositive_TFAE.out 0 5

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