Theorems · Theorem · group theory
IsZGroup.exponent_eq_card
∀ (G : Type u_1) [inst : Group G] [Finite G] [IsZGroup G], Monoid.exponent G = Nat.card G
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Finitestatement and proof · cited by 3,029
- Factproof · cited by 2,726
- Nat.Primeproof · cited by 2,059
- LT.lt.ne'proof · cited by 1,417
- Nat.cardstatement · cited by 844
- Subgroup.subtypeproof · cited by 185
- Monoid.exponentstatement and proof · cited by 128
- Sylowproof · cited by 103
- Sylow.toSubgroupproof · cited by 86
- Nat.card_posproof · cited by 36
- dvd_antisymmproof · cited by 23
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.