mem_center_iff — Mathlib

English

Let M be a semigroup. An element z ∈ M lies in the center of M precisely when z commutes with every element of M.

Русский

Пусть M — полугруппа. Элемент z ∈ M принадлежит центру M тогда и только тогда, когда он коммутирует с каждым элементом M.

LaTeX

$$$ z \in \mathrm{center}(M) \iff \forall m \in M,\ m z = z m $$$

Lean4

@[to_additive mem_addCenter_iff]
theorem mem_center_iff {z : M} : z ∈ center M ↔ IsMulCentral z :=
  Iff.rfl

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