isStrictlyPositive_iff_eq_mul_star_self

English

Equivalent characterization: IsStrictlyPositive(a) iff there exists a unit b with a = b * star(b).

Русский

Эквивалентное описание: IsStrictlyPositive(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_mul_star_self {a : A} :
    IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ a = b * star b :=
  CStarAlgebra.isStrictlyPositive_TFAE.out 0 6

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