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 }