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] : ∑ 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.

theorem Group.nat_card_center_add_sum_card_noncenter_eq_card (G : Type u_1) [Group G] [Finite G] : Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : 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) + ∑ x ∈ (ConjClasses.noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G