mem_center_iff — Mathlib

English

Let R be a (not necessarily unital) ring. An element z lies in the center of R if and only if z commutes with every element of R; that is, for all g in R we have g z = z g.

Русский

Пусть R — кольцо без обязательного наличия единицы. Элемент z принадлежит центру R тогда и только тогда, когда он коммутирует с каждым элементом кольца: для всех g ∈ R выполняется g z = z g.

LaTeX

$$$z \\in \\mathrm{center}(R) \\iff \\forall g \\in R,\\ g z = z g$$$

Lean4

theorem mem_center_iff {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
  Subsemigroup.mem_center_iff

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