nonneg_iff_eq_sqrt_mul_sqrt — Mathlib

English

Reiterates the equivalence between the same nonnegativity characterizations of an element in a C*-algebra as in the previous item.

Русский

Повторение эквивалентностей неотрицательности элемента в C*-алгебре.

LaTeX

$$IsSelfAdjoint a ∧ QuasispectrumRestricts a RealToNNReal$$

Lean4

theorem _root_.CStarAlgebra.nonneg_iff_eq_sqrt_mul_sqrt {a : A} : 0 ≤ a ↔ a = sqrt a * sqrt a :=
  CStarAlgebra.nonneg_TFAE.out 0 1

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