English
For a finite group G, the order of G equals the order of its center plus the sum of the sizes of all nontrivial conjugacy classes.
Русский
Для конечной группы G порядок G равен порядку центра G плюс сумма размеров всех нетривиальных конъюгированных классов.
LaTeX
$$$|Z(G)| + \\sum_{C \\in \\mathrm{noncenter}(G).toFinset} |C| = |G|$$$
Lean4
/-- The **class equation** for finite groups. The cardinality of a group is equal to the size
of its center plus the sum of the size of all its nontrivial conjugacy classes. -/
theorem nat_card_center_add_sum_card_noncenter_eq_card [Finite G] :
Nat.card (Subgroup.center G) + ∑ᶠ x ∈ noncenter G, Nat.card x.carrier = Nat.card G := by
classical
cases nonempty_fintype G
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
congr 1
swap
· convert finsum_cond_eq_sum_of_cond_iff _ _
simp [Set.mem_toFinset]
calc
Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
Fintype.card_congr ((mk_bijOn G).equiv _)
_ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
_ = _ := ?_
rw [Finset.card_eq_sum_ones]
refine Finset.sum_congr rfl ?_
rintro ⟨g⟩ hg
simp only [noncenter, Set.toFinset_setOf, Finset.mem_univ, true_and, Finset.mem_sdiff, Finset.mem_filter,
Set.not_nontrivial_iff] at hg
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
