centralizer — Mathlib

English

Define the centralizer of a subset S of a semigroup M as the subsemigroup of elements that commute with every element of S.

Русский

Определим центральизатор подмножества S полугруппы M как подполугом, состоящий из элементов, которые коммутируют с каждым элементом S.

LaTeX

$$$ centralizer(S) : Subsemigroup M $$$

Lean4

/-- The centralizer of a subset of a semigroup `M`. -/
@[to_additive /-- The centralizer of a subset of an additive semigroup. -/
    ]
def centralizer : Subsemigroup M where
  carrier := S.centralizer
  mul_mem' := Set.mul_mem_centralizer

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