instStarOrderedRing — Mathlib

English

For complex-valued endomorphisms on a Hilbert space, the star-ordered ring structure holds.

Русский

Для комплексно-значных концевых отображений на гильбертовом пространстве сохраняется структура звездообразного упорядоченного кольца.

LaTeX

$$StarOrderedRing (H →L[ℂ] H)$$

Lean4

instance instStarOrderedRing {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :
    StarOrderedRing (H →L[ℂ] H) :=
  instStarOrderedRingRCLike

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