Theorems · Theorem · group theory

Group.nat_card_center_add_sum_card_noncenter_eq_card

∀ (G : Type u_1) [inst : 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.

Defined in: Mathlib.GroupTheory.ClassEquation
Cited by: 1 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites46

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Finsetproof · cited by 13,712
Fintypeproof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
Groupstatement and proof · cited by 6,238
Finset.sumproof · cited by 5,195
Subgroupstatement · cited by 3,593
Finset.univproof · cited by 3,473
Finitestatement and proof · cited by 3,029
Compl.complproof · cited by 2,925
Finset.cardproof · cited by 2,327
Finset.sum_congrproof · cited by 2,323

Cited by1

Results whose statement or proof uses this declaration.

Group.card_center_add_sum_card_noncenter_eq_cardproof · cited by 0