closureCommSemiringOfComm — Mathlib

English

If a set s is pairwise commuting, then the closure of s is a commutative semiring.

Русский

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

LaTeX

$$$CommSemiring(closure(s))$$$

Lean4

/-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring. -/
abbrev closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : CommSemiring (closure s) :=
  { (closure s).toSemiring 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₂) }

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