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) [Group G] [Fintype (ConjClasses G)] [Fintype G] [(x : ConjClasses G) → Fintype ↑(ConjClasses.carrier x)] : (Finset.sum Finset.univ fun (x : ConjClasses G) => (Set.toFinset (ConjClasses.carrier x)).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) [Group G] [Finite G] : (finsum fun (x : ConjClasses G) => Set.ncard (ConjClasses.carrier x)) = Nat.card G

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) [Group G] [Finite G] : (Nat.card ↥(Subgroup.center G) + finsum fun (x : ConjClasses G) => finsum fun (h : x ∈ ConjClasses.noncenter G) => Nat.card ↑(ConjClasses.carrier x)) = Nat.card G

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) [Group G] [(x : ConjClasses G) → Fintype ↑(ConjClasses.carrier x)] [Fintype G] [Fintype ↥(Subgroup.center G)] [Fintype ↑(ConjClasses.noncenter G)] : (Fintype.card ↥(Subgroup.center G) + Finset.sum (Set.toFinset (ConjClasses.noncenter G)) fun (x : ConjClasses G) => (Set.toFinset (ConjClasses.carrier x)).card) = Fintype.card G