English
Let p be a prime, and m a natural number. For all u, v in a commutative semiring with p ∤ a and suitable divisibility conditions, the order of 1 + p^m a modulo p^{n+m} is p^n for every n.
Русский
Пусть p — простое, m ∈ ℕ. При любых u, v в коммутативном полускольном кольце и условиях p ∤ a и подходящих делимости порядок 1 + p^m a по модулю p^{n+m} равен p^n для каждого n.
LaTeX
$$$\\\\forall R [CommSemiring R], \\\\forall u, v \\\\in R, \\\\forall p \\\\in\\\\mathbb{N}, \\\\text{Prime}(p) \\\\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 {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) (a : ℤ) (ha : ¬(p : ℤ) ∣ a) (n : ℕ) :
orderOf (1 + p * a : ZMod (p ^ (n + 1))) = p ^ n :=
by
convert orderOf_one_add_mul_prime_pow hp 1 one_ne_zero _ a ha n using 1
· rw [pow_one]
· have := hp.two_le; cutsat
