center — Mathlib

English

The center of an R-algebra A is the subalgebra consisting of all elements that commute with every element of A.

Русский

Центр R-алгебры A есть подалгебра, состоящая из всех элементов, которые коммутируют со всеми элементами A.

LaTeX

$$$\operatorname{center}(R,A) = \{ a \in A \mid \forall b \in A,\ ba = ab \}$$$

Lean4

/-- The center of an algebra is the set of elements which commute with every element. They form a
subalgebra. -/
@[simps! coe toSubsemiring]
def center : Subalgebra R A :=
  { Subsemiring.center A with algebraMap_mem' := Set.algebraMap_mem_center }

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