Theorems · Theorem · group theory

orderOf_eq_of_pow_and_pow_div_prime

∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ},
  0 < n → x ^ n = 1 → (∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1) → orderOf x = n

If x^n = 1, but x^(n/p) ≠ 1 for all prime factors p of n, then x has order n in G.

Defined in

Mathlib.GroupTheory.OrderOfElement

Cited by

2 results in Mathlib

Foundations

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

Assumes

Monoid