center — Mathlib

English

The center of a ring R is the subring consisting of all elements that commute with every element of R.

Русский

Центр кольца R — это подкольцо, состоящее из всех элементов, коммутирующих с каждым элементом кольца.

LaTeX

$$def center : Subring R := { Subsemiring.center R with carrier := Set.center R }$$

Lean4

/-- The center of a ring `R` is the set of elements that commute with everything in `R` -/
def center : Subring R :=
  { Subsemiring.center R with
    carrier := Set.center R
    neg_mem' := Set.neg_mem_center }

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