Theorems · Theorem · group theory
AddMonoid.ExponentExists.of_finite
∀ {G : Type u} [inst : AddLeftCancelMonoid G] [Finite G], AddMonoid.ExponentExists G- Defined in
- Mathlib.GroupTheory.Exponent
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddLeftCancelMonoidFinite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypeproof · cited by 7,736
- Finset.univproof · cited by 3,473
- Finitestatement and proof · cited by 3,029
- LT.lt.ne'proof · cited by 1,417
- Finset.mem_univproof · cited by 361
- Fintype.ofFiniteproof · cited by 255
- addOrderOfproof · cited by 208
- pos_iff_ne_zeroproof · cited by 180
- IsOfFinAddOrderproof · cited by 105
- Finset.lcmproof · cited by 37
- AddLeftCancelMonoidstatement and proof · cited by 37
- AddMonoid.ExponentExistsstatement · cited by 17
Cited by2
Results whose statement or proof uses this declaration.
- isAddTorsion_of_finiteproof · cited by 3
- AddMonoid.exponent_ne_zero_of_finiteproof · cited by 1