centralizer — Mathlib

English

The centralizer of a set s in a nonunital semiring is the subsemiring consisting of all elements that commute with every element of s.

Русский

Централизатор множества s в непозиционном полусемиринге — это подполусемиринг, состоящий из элементов, которые коммутируют с каждым элементом s.

LaTeX

$$$ \text{centralizer}(s) = \{ x \in R \mid \forall a \in s, a x = x a \} $$$

Lean4

/-- The centralizer of a set as non-unital subsemiring. -/
def centralizer {R} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring R :=
  { Subsemigroup.centralizer s with
    carrier := s.centralizer
    zero_mem' := Set.zero_mem_centralizer
    add_mem' := Set.add_mem_centralizer }

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