le_of_dvd — Mathlib

English

If p > 1, n ≠ 0 and p^pow ∣ n, then pow ≤ p.maxPowDiv(n).

Русский

Если p > 1, n ≠ 0 и p^pow делится на n, то pow ≤ p.maxPowDiv(n).

LaTeX

$$$ (1 < p) \\land (n \\neq 0) \\land p^{\\,pow} \\mid n \\implies pow \\le p.maxPowDiv(n) $$$

Lean4

theorem le_of_dvd {p n pow : ℕ} (hp : 1 < p) (hn : n ≠ 0) (h : p ^ pow ∣ n) : pow ≤ p.maxPowDiv n :=
  by
  have ⟨c, hc⟩ := h
  have : 0 < c := by
    apply Nat.pos_of_ne_zero
    intro h'
    rw [h', mul_zero] at hc
    omega
  simp [hc, base_pow_mul hp this]

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