mem_centralizer_iff — Mathlib

English

An element z lies in the centralizer of s if and only if for every g ∈ s, g z = z g.

Русский

Элемент z принадлежит центральзатору s тогда и только тогда, когда для каждого g ∈ s верно g z = z g.

LaTeX

$$$ z \in centralizer s \;\iff\; \forall g \in s,\; g \cdot z = z \cdot g $$$

Lean4

theorem mem_centralizer_iff {R} [Semiring R] {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
  Iff.rfl

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