adjoinCommSemiringOfIsStarNormal — Mathlib

English

The subalgebra generated by a single element x is commutative if x is normal (IsStarNormal).

Русский

Подалгебра, порождаемая единичным элементом x, коммутативна, если x нормален (IsStarNormal).

LaTeX

$$$\text{if } x\in A\text{ and } IsStarNormal(x)\text{ then } CommSemiring(\operatorname{adjoin}_R(\{x\}:\Set A)).$$$

Lean4

/-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
if `x` is normal. -/
instance adjoinCommSemiringOfIsStarNormal (x : A) [IsStarNormal x] : CommSemiring (adjoin R ({ x } : Set A)) :=
  adjoinCommSemiringOfComm R
    (fun a ha b hb => by
      rw [Set.mem_singleton_iff] at ha hb
      rw [ha, hb])
    fun a ha b hb => by
    rw [Set.mem_singleton_iff] at ha hb
    simpa only [ha, hb] using (star_comm_self' x).symm

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