mem_center_iff — Mathlib

English

An element z lies in the center Z(G) if and only if it commutes with every element of G.

Русский

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

LaTeX

$$$z \in Z(G) \iff \forall g \in G,\; g z = z g$$$

Lean4

@[to_additive]
theorem mem_center_iff {z : G} : z ∈ center G ↔ ∀ g, g * z = z * g :=
  by
  rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

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