adjoinNonUnitalCommRingOfComm — Mathlib

English

If every element of adjoin R s commutes with a, then a commutes with all of adjoin R s.

Русский

Если каждый элемент в adjoin R s коммутирует с a, тогда a коммутирует со всем adjoin R s.

LaTeX

$$commute_of_mem_adjoin_of_forall_mem_commute hb h : Commute a b$$

Lean4

/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a non-unital commutative
ring.

See note [reducible non-instances]. -/
abbrev adjoinNonUnitalCommRingOfComm (R : Type*) {A : Type*} [CommRing R] [NonUnitalRing A] [Module R A]
    [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
    NonUnitalCommRing (adjoin R s) :=
  { (adjoin R s).toNonUnitalRing, adjoinNonUnitalCommSemiringOfComm R hcomm with }

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