English
For all p,m,a ∈ N, (1 + p a)^{p^m} ≡ 1 (mod p^m).
Русский
Для всех p,m,a ∈ ℕ выполняется (1 + p a)^{p^m} ≡ 1 (mod p^m).
LaTeX
$$$\\\\forall p,m,a \\\\in \\\\mathbb{N}, (\\\\mathrm{1} + p a)^{p^{m}} \\\\equiv 1 \\\\pmod{p^{m}}$$$
Lean4
theorem pow_pow_modEq_one (p m a : ℕ) : (1 + p * a) ^ (p ^ m) ≡ 1 [MOD p ^ m] := by
induction m with
| zero => exact Nat.modEq_one
| succ m hm =>
rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm
obtain ⟨d, hd⟩ := hm
rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd
rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow, one_mul,
Nat.choose_zero_right, Nat.cast_one]
refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)
simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]
refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)
cases m
· rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
cases k <;> simp [← hd, mul_assoc, pow_succ']
· cases k <;> simp [mul_assoc, pow_succ']
