adjoinNonUnitalCommSemiringOfComm

English

A corollary: if s is pairwise commutative, adjoin R s forms a nonunital commutative semiring with the canonical identifications.

Русский

Следствие: если s парно коммутирует, adjoin R s образует ненулевой коммутативный полупром вместе с каноническими тождествами.

LaTeX

$$abbrev adjoinNonUnitalCommSemiringOfComm (R) {A} (hcomm) : NonUnitalCommSemiring (adjoin R s)$$

Lean4

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

See note [reducible non-instances]. -/
abbrev adjoinNonUnitalCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
    NonUnitalCommSemiring (adjoin R s) :=
  { (adjoin R s).toNonUnitalSemiring with
    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
      have := adjoin_le_centralizer_centralizer R s
      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }

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