English
If x^n = 1 and for every prime p dividing n we have x^{n/p} ≠ 1, then ord(x) = n.
Русский
Если x^n = 1 и для каждого простого p, делящего n, выполняется x^{n/p} ≠ 1, тогда ord(x) = n.
LaTeX
$$$ \forall G [Monoid G], \forall x : G, \forall n > 0, (x^n = 1) ∧ (\forall p \text{ prime}, p \mid n → x^{n/p} ≠ 1) \Rightarrow ord(x) = n$$$
Lean4
/-- If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `n`,
then `x` has order `n` in `G`. -/
@[to_additive addOrderOf_eq_of_nsmul_and_div_prime_nsmul /-- If `n * x = 0`, but `n/p * x ≠ 0` for
all prime factors `p` of `n`, then `x` has order `n` in `G`. -/
]
theorem orderOf_eq_of_pow_and_pow_div_prime (hn : 0 < n) (hx : x ^ n = 1)
(hd : ∀ p : ℕ, p.Prime → p ∣ n → x ^ (n / p) ≠ 1) : orderOf x = n := by
-- Let `a` be `n/(orderOf x)`, and show `a = 1`
obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)
suffices a = 1 by
simp [this, ha]
-- Assume `a` is not one...
by_contra h
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n :=
by
obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
rw [hb, ← mul_assoc] at ha
exact Dvd.intro_left (orderOf x * b) ha.symm
refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_
rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
· exact Nat.minFac_dvd a
· rw [isOfFinOrder_iff_pow_eq_one]
exact Exists.intro n (id ⟨hn, hx⟩)
