center_eq_iInf — Mathlib

English

If the closure of a subset S of a group G is the whole group, then the center Z(G) equals the intersection over g in S of the centralizers of the cyclic subgroups generated by g.

Русский

Если замыкание S в группе G равняется всей группе, то центр Z(G) равен пересечению по всем g ∈ S центральизаторов порождаемых g циклических подгрупп.

LaTeX

$$$Z(G) = \bigcap_{g \in S} \mathrm{C}_G(\mathrm{zpowers}(g))$$$

Lean4

@[to_additive]
theorem center_eq_iInf (S : Set G) (hS : closure S = ⊤) : center G = ⨅ g ∈ S, centralizer (zpowers g) := by
  rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]

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