adjoinCommRingOfIsStarNormal — Mathlib

English

The star-subalgebra generated by a single x is a commutative ring when x is normal.

Русский

Звездо-подалгебра, порождаемая одним элементом x, является коммутативным кольцом, если x нормален.

LaTeX

$$$\text{instance } adjoinCommRingOfIsStarNormal (R) {A} (x) [IsStarNormal x] : CommRing(\operatorname{adjoin}_R(\{x\}))$$$

Lean4

/-- The star subalgebra `StarSubalgebra.adjoin R {x}` generated by a single `x : A` is commutative
if `x` is normal. -/
instance adjoinCommRingOfIsStarNormal (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A]
    [StarRing A] [StarModule R A] (x : A) [IsStarNormal x] : CommRing (adjoin R ({ x } : Set A)) :=
  { (adjoin R ({ x } : Set A)).toSubalgebra.toRing with mul_comm := mul_comm }

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