mem_centralizer_iff — Mathlib

English

An element g belongs to the centralizer of s if and only if g commutes with every element of s.

Русский

Элемент g принадлежит центроцентрализатору s тогда и только тогда, когда он коммутирует с каждым элементом s.

LaTeX

$$g \in centralizer(s) \iff \forall h \in s,\; h g = g h$$

Lean4

@[to_additive]
theorem mem_centralizer_iff {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h :=
  Iff.rfl

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