English
For natural p, n, p^(p.maxPowDiv n) divides n.
Русский
Для натурального p и n верно p^{p.maxPowDiv n} делится на n.
LaTeX
$$$ p^{\\,p.maxPowDiv(n)} \\mid n $$$
Lean4
theorem pow_dvd (p n : ℕ) : p ^ (p.maxPowDiv n) ∣ n :=
by
dsimp [maxPowDiv]
rw [go]
by_cases h : (1 < p ∧ 0 < n ∧ n % p = 0)
· have : n / p < n := by apply Nat.div_lt_self <;> aesop
rw [if_pos h]
have ⟨c, hc⟩ := pow_dvd p (n / p)
rw [go_succ, pow_succ]
nth_rw 2 [← mod_add_div' n p]
rw [h.right.right, zero_add]
exact ⟨c, by nth_rw 1 [hc]; ac_rfl⟩
· rw [if_neg h]
simp