# Documentation

Mathlib.GroupTheory.ClassEquation

# Class Equation #

This file establishes the class equation for finite groups.

## Main statements #

• Group.card_center_add_sum_card_noncenter_eq_card: 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. Also Group.nat_card_center_add_sum_card_noncenter_eq_card.
theorem sum_conjClasses_card_eq_card (G : Type u) [] [] [] [(x : ) → ] :
(Finset.sum Finset.univ fun x => ) =

Conjugacy classes form a partition of G, stated in terms of cardinality.

theorem Group.sum_card_conj_classes_eq_card (G : Type u) [] [] :
∑ᶠ (x : ), =

Conjugacy classes form a partition of G, stated in terms of cardinality.

theorem Group.nat_card_center_add_sum_card_noncenter_eq_card (G : Type u) [] [] :
Nat.card { x // } + ∑ᶠ (x : ) (_ : ), =

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 Group.card_center_add_sum_card_noncenter_eq_card (G : Type u_1) [] [(x : ) → ] [] [Fintype { x // }] [] :
(Fintype.card { x // } + Finset.sum () fun x => ) =