instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal

English

The star of any element is contained in the elemental subalgebra generated by that element.

Русский

Звезда любого элемента принадлежит элементальной подалгебре, сгенерированной этим элементом.

LaTeX

$$star x ∈ elemental R x$$

Lean4

/-- The `elemental` generated by a normal element is commutative. -/
instance {R A} [CommRing R] [StarRing R] [TopologicalSpace A] [Ring A] [Algebra R A] [StarRing A] [StarModule R A]
    [IsTopologicalRing A] [ContinuousStar A] [T2Space A] {x : A} [IsStarNormal x] : CommRing (elemental R x) :=
  StarSubalgebra.commRingTopologicalClosure _ mul_comm

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