Documentation

Mathlib.Data.Nat.PadicValNat

The p-adic valuation on natural numbers #

source
def padicValNat (p n : ℕ) :
ℕ

For p ≠ 1, the p-adic valuation of a natural n ≠ 0 is the largest natural number k such that p^k divides n. If n = 0 or p = 1, then padicValNat p n defaults to 0.

Equations
Instances For
    source
    @[simp]
    theorem Nat.divMaxPow_mul_pow_padicValNat (p n : ℕ) :
    n.divMaxPow p * p ^ padicValNat p n = n
    source
    theorem Nat.padicValNat_def {p n : ℕ} :
    padicValNat p n = multiplicity p n
    source
    @[simp]
    theorem padicValNat_zero_left (n : ℕ) :
    padicValNat 0 n = 0
    source
    @[simp]
    theorem padicValNat_one_left (n : ℕ) :
    padicValNat 1 n = 0
    source
    @[simp]
    theorem padicValNat_zero_right (p : ℕ) :
    padicValNat p 0 = 0
    source
    theorem Nat.maxPowDvdDiv_of_not_dvd {p n : ℕ} (h : ¬p ∣ n) :
    p.maxPowDvdDiv n = (0, n)
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_one_right (p : ℕ) :
    p.maxPowDvdDiv 1 = (0, 1)
    source
    @[simp]
    theorem padicValNat_one_right (p : ℕ) :
    padicValNat p 1 = 0
    source
    @[simp]
    theorem Nat.divMaxPow_one_left (p : ℕ) :
    divMaxPow 1 p = 1
    source
    @[simp]
    theorem Nat.pow_padicValNat_mul_divMaxPow (p n : ℕ) :
    p ^ padicValNat p n * n.divMaxPow p = n
    source
    theorem pow_padicValNat_dvd {p n : ℕ} :
    p ^ padicValNat p n ∣ n
    source
    theorem Nat.padicValNat_lt_self {p n : ℕ} (hn : n ≠ 0) :
    padicValNat p n < n
    source
    theorem Nat.padicValNat_le_self {p : ℕ} (n : ℕ) :
    padicValNat p n ≤ n
    source
    theorem Nat.pow_dvd_iff_le_padicValNat {p k n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :
    p ^ k ∣ n ↔ k ≤ padicValNat p n

    If p > 1, n > 0, then the first component of maxPowDvdDiv is the maximal power of p that divides n.

    source
    theorem Nat.maxPowDvdDiv_of_pow_mul_eq {p n k l : ℕ} (hn : n ≠ 0) (h : p ^ k * l = n) (hl : ¬p ∣ l) :
    p.maxPowDvdDiv n = (k, l)
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :
    p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)
    source
    @[simp]
    theorem padicValNat_base_pow_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (k : ℕ) :
    padicValNat p (p ^ k * n) = padicValNat p n + k
    source
    @[simp]
    theorem Nat.divMaxPow_base_pow_mul {p : ℕ} (hp : p ≠ 0) (n k : ℕ) :
    (p ^ k * n).divMaxPow p = n.divMaxPow p
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :
    p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)
    source
    @[simp]
    theorem padicValNat_base_mul {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) :
    padicValNat p (p * n) = padicValNat p n + 1
    source
    @[simp]
    theorem Nat.divMaxPow_base_mul {p : ℕ} (hp : p ≠ 0) (n : ℕ) :
    (p * n).divMaxPow p = n.divMaxPow p
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :
    p.maxPowDvdDiv (p ^ k) = (k, 1)
    source
    @[simp]
    theorem padicValNat_base_pow {p : ℕ} (hp : 1 < p) (k : ℕ) :
    padicValNat p (p ^ k) = k
    source
    @[simp]
    theorem Nat.divMaxPow_base_pow {p : ℕ} (hp : p ≠ 0) (k : ℕ) :
    (p ^ k).divMaxPow p = 1
    source
    @[simp]
    theorem Nat.maxPowDvdDiv_self {p : ℕ} (hp : 1 < p) :
    p.maxPowDvdDiv p = (1, 1)
    source
    @[simp]
    theorem padicValNat_base {p : ℕ} (hp : 1 < p) :
    padicValNat p p = 1
    source
    @[simp]
    theorem Nat.divMaxPow_self {p : ℕ} (hp : p ≠ 0) :
    p.divMaxPow p = 1
    source
    @[simp]
    theorem Nat.fst_maxPowDvdDiv (p n : ℕ) :
    (p.maxPowDvdDiv n).1 = padicValNat p n
    source
    @[simp]
    theorem Nat.snd_maxPowDvdDiv (p n : ℕ) :
    (p.maxPowDvdDiv n).2 = n.divMaxPow p