instCommSemiringSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal

English

For any x in A, x belongs to the elemental subalgebra generated by x.

Русский

Для любого x в A элемент x принадлежит элементальной подалгебре, сгенерированной x.

LaTeX

$$x ∈ elemental R x$$

Lean4

/-- The `elemental` star subalgebra generated by a normal element is commutative. -/
instance [T2Space A] {x : A} [IsStarNormal x] : CommSemiring (elemental R x) :=
  StarSubalgebra.commSemiringTopologicalClosure _ mul_comm

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