mem_centralizer_iff — Mathlib

English

An element z is in the centralizer of S if and only if z commutes with every element of S.

Русский

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

LaTeX

$$$ z \\in centralizer(S) \\iff \\forall g \\in S, g z = z g $$$

Lean4

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

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