sum_card_conj_classes_eq_card — Mathlib

English

For a finite group G, the finsum over all conjugacy classes of the size of each class equals the order of 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_card_conj_classes_eq_card [Finite G] : ∑ᶠ x : ConjClasses G, x.carrier.ncard = Nat.card G := by
  classical
  cases nonempty_fintype G
  rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
  simp [Set.ncard_eq_toFinset_card']

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