English
Let p be a prime, m a positive integer, and a ∈ Z with p ∤ a. Then for all n, the order of 1 + p^m a in Z/(p^{n+m})Z is p^n.
Русский
Пусть p — простое число, m > 0 и a ∈ Z такой, что p не делит a. Тогда для любого n порядок элемента 1 + p^m a в Z/(p^{n+m})Z равен p^n.
LaTeX
$$$\\\\forall p \\\\in \\mathbb{N}, \\\\text{Prime}(p) \\\\wedge m \\\\ge 1, \\\\forall a \\\\in \\\\mathbb{Z}, \\\\neg (p \\\\mid a) \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, \\\\operatorname{orderOf}(1 + p^{m} a \\\\bmod p^{n+m}) = p^{n}.$$$
Lean4
theorem orderOf_one_add_mul_prime_pow {p : ℕ} (hp : p.Prime) (m : ℕ) (hm0 : m ≠ 0) (hpm : m + 2 ≤ p * m) (a : ℤ)
(ha : ¬(p : ℤ) ∣ a) (n : ℕ) : orderOf (1 + p ^ m * a : ZMod (p ^ (n + m))) = p ^ n := by
match n with
| 0 => rw [← Nat.cast_pow, zero_add m, ZMod.natCast_self]; simp
| n + 1 =>
have := Fact.mk hp
have :=
exists_one_add_mul_pow_prime_pow_eq (R := ZMod (p ^ (n + 1 + m))) (u := p ^ m) (v := p) hp (dvd_pow_self _ hm0) ?_
a
· apply orderOf_eq_prime_pow
· obtain ⟨y, hy⟩ := this n
rw [hy, ← pow_add, add_eq_left, mul_add, ← mul_assoc, ← pow_succ]
simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]
rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm, pow_succ,
Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
· obtain ⟨y, hy⟩ := this (n + 1)
rw [hy, ← pow_add, ← Nat.cast_pow]
simp
· rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]
exact pow_dvd_pow _ hpm
