pow_dvd — Mathlib

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

Похожие утверждения