Mathlib Map

Theorems · Definition · group theory

AddMonoid.ExponentExists

(G : Type u) → [AddMonoid G] → Prop

A predicate on an additive monoid saying that there is a positive integer n such that n • g = 0 for all g.

Defined in
Mathlib.GroupTheory.Exponent
Cited by
17 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddMonoid.exponent · cited by 70AddMonoid.exponentAddMonoid.exponent_nsmul_eq_zero · cited by 12AddMonoid.exponent_nsmul_…AddMonoid.exponent_eq_zero_iff · cited by 5AddMonoid.exponent_eq_zer…AddMonoid.exponent_ne_zero · cited by 4AddMonoid.exponent_ne_zeroExponentExists.isAddTorsion · cited by 2ExponentExists.isAddTorsi…AddMonoid.ExponentExists.addOrderOf_pos · cited by 2ExponentExists.addOrderOf…AddMonoid.ExponentExists.exponent_ne_zero · cited by 2ExponentExists.exponent_n…AddMonoid.ExponentExists.exponent_pos · cited by 2ExponentExists.exponent_p…AddMonoid.ExponentExists.of_finite · cited by 2ExponentExists.of_finiteAddMonoid.exponent_eq_iSup_addOrderOf · cited by 2AddMonoid.exponent_eq_iSu…AddMonoid.exponent_eq_zero_addOrder_zero · cited by 2AddMonoid.exponent_eq_zer…AddMonoid.exponent_pos · cited by 1AddMonoid.exponent_posAddMonoid.addOrderOf_le_exponent · cited by 1AddMonoid.addOrderOf_le_e…AddMonoid.exists_addOrderOf_eq_exponent · cited by 1AddMonoid.exists_addOrder…AddMonoid.ExponentExists.isOfFinAddOrder · cited by 1ExponentExists.isOfFinAdd…AddMonoid · cited by 2864AddMonoidAddMonoid.ExponentExistsCITED BYCITES

Cites1

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

Cited by18

Results whose statement or proof uses this declaration.