closureNonUnitalCommSemiringOfComm

English

If every pair of elements of s commute, then closure(s) is a nonunital commutative semiring.

Русский

Если все пары элементов множества s коммутируют, то closure(s) образует неединичный коммутативный полусемиринг.

LaTeX

$$If ∀ x,y ∈ s, x y = y x, then closure(s) is a NonUnitalCommSemiring.$$

Lean4

/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
semiring. -/
abbrev closureNonUnitalCommSemiringOfComm {R : Type*} [NonUnitalSemiring R] {s : Set R}
    (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : NonUnitalCommSemiring (closure s) :=
  { NonUnitalSubsemiringClass.toNonUnitalSemiring (closure s) with
    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
      have := closure_le_centralizer_centralizer s
      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }

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