sum_conjClasses_card_eq_card — Mathlib

English

In any finite group G, the sum over all conjugacy classes of the size of each class equals the order of G.

Русский

В конечной группе G сумма по всем конъюгированным классам их размеров равна порядку группы G.

LaTeX

$$$\\sum_{C \\in \\mathrm{ConjClasses}(G)} |C| = |G|$$$

Lean4

/-- Conjugacy classes form a partition of G, stated in terms of cardinality. -/
theorem sum_conjClasses_card_eq_card [Fintype <| ConjClasses G] [Fintype G] [∀ x : ConjClasses G, Fintype x.carrier] :
    ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G :=
  by
  suffices (Σ x : ConjClasses G, x.carrier) ≃ G by simpa using (Fintype.card_congr this)
  simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk

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