Theorems · Definition · group theory
AddMonoid.exponent
(G : Type u) → [AddMonoid G] → ℕ
The exponent of an additive group is the smallest positive integer n such that
n • g = 0 for all g ∈ G if it exists, otherwise it is zero by convention.
- Defined in
- Mathlib.GroupTheory.Exponent
- Cited by
- 70 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- Nat.findproof · cited by 139
- AddMonoid.ExponentExistsproof · cited by 17
Cited by74
Results whose statement or proof uses this declaration.
- AddMonoid.exponent_nsmul_eq_zerostatement · cited by 12
- AddMonoid.addOrder_dvd_exponentstatement · cited by 10
- IsAddCyclic.exponent_eq_cardstatement and proof · cited by 5
- AddMonoid.exponent_dvdstatement · cited by 5
- AddMonoid.exponent_dvd_of_forall_nsmul_eq_zerostatement · cited by 5
- AddMonoid.exponent_eq_zero_iffstatement · cited by 5
- AddMonoid.exponent_ne_zerostatement · cited by 4
- AddMonoidHom.exponent_dvdstatement and proof · cited by 4
- AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zerostatement and proof · cited by 4
- IsAddKleinFour.exponent_twostatement · cited by 4
- AddMonoid.exponent_min'statement · cited by 3
- AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finitestatement and proof · cited by 3