center_eq_infi' — Mathlib

English

Let S be a subset with closure S = ⊤. Then the center Z(G) equals the infimum over all g in S of the centralizer of the cyclic subgroup generated by g, interpreted via elements of S.

Русский

Пусть S —subset с замыканием ⊤. Тогда центр Z(G) равен пересечению по элементам g из S центральизаторов циклических подгрупп, порождаемых g.

LaTeX

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

Lean4

@[to_additive]
theorem center_eq_infi' (S : Set G) (hS : closure S = ⊤) : center G = ⨅ g : S, centralizer (zpowers (g : G)) := by
  rw [center_eq_iInf S hS, ← iInf_subtype'']

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