centralizer — Mathlib

English

For a set s ⊆ A, the centralizer centralizes s together with its star-closure; it forms a StarSubalgebra of A consisting of elements commuting with every element of s ∪ s*.

Русский

Централизатор s ∪ s* образует звездную подсалгебру, состоящую из элементов, коммутирующих с каждым элементом s ∪ s*.

LaTeX

$$def centralizer (s : Set A) : StarSubalgebra R A$$

Lean4

/-- The centralizer, or commutant, of the star-closure of a set as a star subalgebra. -/
def centralizer (s : Set A) : StarSubalgebra R A
    where
  toSubalgebra := Subalgebra.centralizer R (s ∪ star s)
  star_mem' := Set.star_mem_centralizer

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