Documentation

Mathlib.GroupTheory.ClassEquation

Class Equation #

This file establishes the class equation for finite groups.

Main statements #

theorem sum_conjClasses_card_eq_card (G : Type u_1) [Group G] [Fintype (ConjClasses G)] [Fintype G] [(x : ConjClasses G) → Fintype x.carrier] :
x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G

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

theorem Group.sum_card_conj_classes_eq_card (G : Type u_1) [Group G] [Finite G] :
∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

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

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_2) [Group G] [(x : ConjClasses G) → Fintype x.carrier] [Fintype G] [Fintype (Subgroup.center G)] [Fintype (ConjClasses.noncenter G)] :
Fintype.card (Subgroup.center G) + x(ConjClasses.noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G