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_1) [Group G] [Fintype (ConjClasses G)] [Fintype G] [(x : ConjClasses G) → Fintype ↑x.carrier] : (Finset.univ.sum fun (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] : (finsum fun (x : ConjClasses G) => x.carrier.ncard) = 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_1) [Group G] [Finite G] : (Nat.card ↥(Subgroup.center G) + finsum fun (x : ConjClasses G) => finsum fun (h : x ∈ ConjClasses.noncenter G) => Nat.card ↑x.carrier) = 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_2) [Group G] [(x : ConjClasses G) → Fintype ↑x.carrier] [Fintype G] [Fintype ↥(Subgroup.center G)] [Fintype ↑(ConjClasses.noncenter G)] : (Fintype.card ↥(Subgroup.center G) + (ConjClasses.noncenter G).toFinset.sum fun (x : ConjClasses G) => x.carrier.toFinset.card) = Fintype.card G