centralizer — Mathlib

English

The centralizer of a set s in A forms a subalgebra, namely the centralizer subalgebra.

Русский

Централизатор множества s в A образует подалгебру, называемую центральизатором.

LaTeX

$$$\mathrm{centralizer}(R,s) \text{ is a Subalgebra of } A$$$

Lean4

/-- The centralizer of a set as a subalgebra. -/
def centralizer (s : Set A) : Subalgebra R A :=
  { Subsemiring.centralizer s with algebraMap_mem' := Set.algebraMap_mem_centralizer }

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