Theorems · Theorem · group theory

addOrderOf_eq_of_nsmul_and_div_prime_nsmul

∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ},
  0 < n → n • x = 0 → (∀ (p : ℕ), Nat.Prime p → p ∣ n → (n / p) • x ≠ 0) → addOrderOf x = n

If n * x = 0, but n/p * x ≠ 0 for all prime factors p of n, then x has order n in G.

Defined in

Mathlib.GroupTheory.OrderOfElement

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoid