Theorems · Theorem · group theory
sum_conjClasses_card_eq_card
∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype (ConjClasses G)] [inst_2 : Fintype G] [inst_3 : (x : ConjClasses G) → Fintype ↑x.carrier], ∑ x, x.carrier.toFinset.card = Fintype.card G
Conjugacy classes form a partition of G, stated in terms of cardinality.
- Defined in
- Mathlib.GroupTheory.ClassEquation
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivproof · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Groupstatement and proof · cited by 6,238
- Finset.sumstatement · cited by 5,195
- Finset.univstatement and proof · cited by 3,473
- Finset.cardstatement · cited by 2,327
- Finset.sum_congrproof · cited by 2,323
- Fintype.cardstatement and proof · cited by 1,386
- Set.toFinsetstatement · cited by 217
- Fintype.card_congrproof · cited by 67
- Set.toFinset_cardproof · cited by 63
Cited by1
Results whose statement or proof uses this declaration.
- Group.nat_card_center_add_sum_card_noncenter_eq_cardproof · cited by 1