mem_centralizer_iff_commutator_eq_one

English

For any g ∈ G and any finite subset s ⊂ G, g belongs to centralizer s exactly when h g h^{-1} g^{-1} = 1 for all h ∈ s.

Русский

Для любого g и конечного подмножества s ⊂ G верно: g ∈ centralizer(s) тогда и только тогда, когда h g h^{-1} g^{-1} = 1 для всех h ∈ s.

LaTeX

$$g \in centralizer(s) \iff \forall h \in s,\; h g h^{-1} g^{-1} = 1$$

Lean4

@[to_additive]
theorem mem_centralizer_iff_commutator_eq_one {g : G} {s : Set G} :
    g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1 := by
  simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]

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