mem_centralizer_iff — Mathlib

English

For a subset S of M in a semigroup, an element c ∈ M lies in the centralizer of S exactly when c commutes with every element of S.

Русский

Для подмножества S множества M элемент c принадлежит центральизатору S тогда и только тогда, когда c коммутирует с каждым элементом S.

LaTeX

$$$ c \in \mathrm{centralizer}(S) \iff \forall m \in S,\ m c = c m $$$

Lean4

@[to_additive mem_addCentralizer]
theorem mem_centralizer_iff {c : M} : c ∈ centralizer S ↔ ∀ m ∈ S, m * c = c * m :=
  Iff.rfl

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