instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal

English

If x ∈ A is IsStarNormal, then the elemental subalgebra generated by x yields a commutative sub-C*-algebra.

Русский

Если x ∈ A является IsStarNormal, то элементарная подалгебра, порожденная x, образует коммутативную под-C*-алгебру.

LaTeX

$$IsStarNormal(x) ⇒ CommCStarAlgebra(StarSubalgebra.elemental Complex x)$$

Lean4

noncomputable instance [CStarAlgebra A] (x : A) [IsStarNormal x] : CommCStarAlgebra (StarAlgebra.elemental ℂ x) where

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