HepLean Documentation

Mathlib.NumberTheory.Padics.PadicVal.Defs

p-adic Valuation #

This file defines the p-adic valuation on ℕ, ℤ, and ℚ.

The p-adic valuation on ℚ is the difference of the multiplicities of p in the numerator and denominator of q. This function obeys the standard properties of a valuation, with the appropriate assumptions on p. The p-adic valuations on ℕ and ℤ agree with that on ℚ.

The valuation induces a norm on ℚ. This norm is defined in padicNorm.lean.

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 q defaults to 0.

Equations
Instances For
    source
    theorem padicValNat_def' {p : ℕ} {n : ℕ} (hp : p ≠ 1) (hn : 0 < n) :
    padicValNat p n = multiplicity p n
    source
    theorem padicValNat_def {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) :
    padicValNat p n = multiplicity p n

    A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

    source
    theorem padicValNat_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) :
    ↑(padicValNat p n) = emultiplicity p n

    A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

    source
    @[simp]
    theorem padicValNat.zero {p : ℕ} :
    padicValNat p 0 = 0

    padicValNat p 0 is 0 for any p.

    source
    @[simp]
    theorem padicValNat.one {p : ℕ} :
    padicValNat p 1 = 0

    padicValNat p 1 is 0 for any p.

    source
    @[simp]
    theorem padicValNat.eq_zero_iff {p : ℕ} {n : ℕ} :
    padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
    source
    theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a : ℕ} {b : ℕ} {n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList
    source
    @[deprecated le_emultiplicity_iff_replicate_subperm_primeFactorsList]
    theorem le_multiplicity_iff_replicate_subperm_factors {a : ℕ} {b : ℕ} {n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList

    Alias of le_emultiplicity_iff_replicate_subperm_primeFactorsList.

    source
    theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a : ℕ} {b : ℕ} {n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList
    source
    @[deprecated le_padicValNat_iff_replicate_subperm_primeFactorsList]
    theorem le_padicValNat_iff_replicate_subperm_factors {a : ℕ} {b : ℕ} {n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList

    Alias of le_padicValNat_iff_replicate_subperm_primeFactorsList.