index_center_le_pow — Mathlib

English

Under the same hypotheses, the index of the center is bounded by the commutator set size raised to the rank of the group: [G:Z(G)] ≤ |commutatorSet(G)|^{rank(G)}.

Русский

При тех же предположениях индекс центра ограничен мощностью множества коммутаторов в степени ранга группы: [G:Z(G)] ≤ |commutatorSet(G)|^{rank(G)}.

LaTeX

$$$[G:\mathrm{Z}(G)] \le \big|\mathrm{commutatorSet}(G)\big|^{\mathrm{rank}(G)}$$$

Lean4

theorem index_center_le_pow : (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G :=
  by
  obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
  rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
  exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)

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