English
If x is IsStarNormal, then the elemental subalgebra is a nonunital commutative semiring (hence commutative under multiplication).
Русский
Если x является IsStarNormal, то элементальная подпалгебра образует неединичный коммутативный полупространство, то есть умножение коммутирует.
LaTeX
$$$\\operatorname{NonUnitalCommSemiring}(\\operatorname{elemental}_R(x)).$$$
Lean4
instance [T2Space A] {x : A} [IsStarNormal x] : NonUnitalCommSemiring (elemental R x) :=
nonUnitalCommSemiringTopologicalClosure _ <|
by
letI : NonUnitalCommSemiring (adjoin R { x }) :=
by
refine NonUnitalStarAlgebra.adjoinNonUnitalCommSemiringOfComm R ?_ ?_
all_goals
intro y hy z hz
rw [Set.mem_singleton_iff] at hy hz
rw [hy, hz]
exact (star_comm_self' x).symm
exact fun _ _ => mul_comm _ _
