commute_of_mem_adjoin_self — Mathlib

English

The adjoin of s forms a NonUnitalCommRing when elements commute pairwise and with stars; i.e. the generated subring is commutative and nonunital.

Русский

Объединение множества s образует ненулевое коммутативное кольцо без единицы при условии взаимной коммутативности элементов и с их звездой.

LaTeX

$$adjoinNonUnitalCommRingOfComm (R) {A} ...$$

Lean4

theorem commute_of_mem_adjoin_self {a b : A} [IsStarNormal a] (hb : b ∈ adjoin R { a }) : Commute a b :=
  commute_of_mem_adjoin_singleton_of_commute hb rfl (isStarNormal_iff a |>.mp inferInstance).symm

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