instStarOrderedRing — Mathlib

English

The unitization A⁺¹ becomes a StarOrderedRing with the induced involution, i.e., the star operation and the order extend from A to A⁺¹.

Русский

Единичизация A⁺¹ образует StarOrderedRing: операция звёздочки и порядок распространяются на A⁺¹ от A.

LaTeX

$$$A^{+1}$ is a StarOrderedRing with the natural involution extending that of $A$.$$

Lean4

instance instStarOrderedRing : StarOrderedRing A⁺¹ :=
  CStarAlgebra.spectralOrderedRing _

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