centralizer — Mathlib

English

The centralizer of a set s is a nonunital subalgebra generated by all elements commuting with s.

Русский

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

LaTeX

$$def centralizer (s) : NonUnitalSubalgebra R A$$

Lean4

/-- The centralizer of a set as a non-unital subalgebra. -/
def centralizer (s : Set A) : NonUnitalSubalgebra R A
    where
  toNonUnitalSubsemiring := NonUnitalSubsemiring.centralizer s
  smul_mem' := Set.smul_mem_centralizer

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