Mathlib Map

Theorems · Theorem · group theory

isOfFinAddOrder_iff_nsmul_eq_zero

∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x ↔ ∃ n, 0 < n ∧ n • x = 0
Defined in
Mathlib.GroupTheory.OrderOfElement
Cited by
27 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext, Quot.sound
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

not_isOfFinAddOrder_of_isAddTorsionFree · cited by 7not_isOfFinAddOrder_of_is…IsOfFinAddOrder.exists_nsmul_eq_zero · cited by 6IsOfFinAddOrder.exists_ns…isAddTorsionFree_iff_not_isOfFinAddOrder · cited by 4isAddTorsionFree_iff_not_…ExponentExists.isAddTorsion · cited by 2ExponentExists.isAddTorsi…not_isOfFinAddOrder_of_injective_nsmul · cited by 2not_isOfFinAddOrder_of_in…AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom · cited by 2AddCommGroup.isAddTorsion…injective_zsmul_iff_not_isOfFinAddOrder · cited by 2injective_zsmul_iff_not_i…IsAddTorsion.extension_closed · cited by 2IsAddTorsion.extension_cl…IsOfFinAddOrder.zero · cited by 2IsOfFinAddOrder.zeroIsAddTorsion.module_of_torsion · cited by 2IsAddTorsion.module_of_to…infinite_not_isOfFinAddOrder · cited by 2infinite_not_isOfFinAddOr…AddMonoidHom.isOfFinAddOrder · cited by 2AddMonoidHom.isOfFinAddOr…isOfFinAddOrder_neg_iff · cited by 2isOfFinAddOrder_neg_iffisAddTorsion_iff_isTorsion_int · cited by 2isAddTorsion_iff_isTorsio…AddRightCancelMonoid.finite_multiples · cited by 1AddRightCancelMonoid.fini…AddMonoid · cited by 2864AddMonoidIsOfFinAddOrder · cited by 105IsOfFinAddOrderisPeriodicPt_add_iff_nsmul_eq_zero · cited by 10isPeriodicPt_add_iff_nsmu…Function.mem_periodicPts · cited by 2Function.mem_periodicPtsisOfFinAddOrder_iff_nsmul_eq_…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by27

Results whose statement or proof uses this declaration.