one_le_padicValNat_of_dvd — Mathlib

English

If p is prime, n ≠ 0 and p divides n, then 1 ≤ padicValNat p n.

Русский

Если p — простое, n ≠ 0 и p делит n, то 1 ≤ padicValNat p n.

LaTeX

$$$1 \le \mathrm{padicValNat}(p,n)$ при $p|n$, $n\neq 0$ (при условии, что pPrime).$$

Lean4

theorem one_le_padicValNat_of_dvd {n : ℕ} [hp : Fact p.Prime] (hn : n ≠ 0) (div : p ∣ n) : 1 ≤ padicValNat p n := by
  rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn, ← pow_dvd_iff_le_emultiplicity, pow_one]

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