finiteIndex_center — Mathlib

English

If a group G has a finite commutator set and is finitely generated, then the center Z(G) has finite index in G.

Русский

Пусть G — группа с конечным множеством коммутаторов и с конечной порождающей множество; тогда Z(G) имеет конечный индекс в G.

LaTeX

$$$\Big( Finite(\mathrm{commutatorSet}(G)) \land FG(G) \Big) \Rightarrow [G:\mathrm{Z}(G)] < \infty$$$

Lean4

instance finiteIndex_center : FiniteIndex (center G) :=
  by
  obtain ⟨S, -, hS⟩ := Group.rank_spec G
  exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩

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