Theorems · Theorem · group theory
addOrderOf_nsmul
∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [Finite G] {n : ℕ} (x : G),
addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd nThis is the same as addOrderOf_nsmul' and
addOrderOf_nsmul but with one assumption less which is automatic in the case of a
finite cancellative additive monoid.
- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 69 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.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finitestatement and proof · cited by 3,029
- addOrderOfstatement · cited by 208
- AddLeftCancelMonoidstatement and proof · cited by 37
- isOfFinAddOrder_of_finiteproof · cited by 10
- IsOfFinAddOrder.addOrderOf_nsmulproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- IsAddCyclic.card_nsmulAddMonoidHom_rangeproof · cited by 1
- IsAddCyclic.card_nsmul_eq_zero_leproof · cited by 1