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.

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
    theorem padicValNat_def {p : } [hp : Fact (Nat.Prime p)] {n : } (hn : 0 < n) :
    padicValNat p n = (multiplicity p n).get

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

    theorem padicValNat_def' {p : } {n : } (hp : p 1) (hn : 0 < n) :
    @[simp]
    theorem padicValNat.zero {p : } :

    padicValNat p 0 is 0 for any p.

    @[simp]
    theorem padicValNat.one {p : } :

    padicValNat p 1 is 0 for any p.

    @[simp]
    theorem padicValNat.eq_zero_iff {p : } {n : } :
    padicValNat p n = 0 p = 1 n = 0 ¬p n
    theorem le_multiplicity_iff_replicate_subperm_primeFactorsList {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
    n multiplicity a b (List.replicate n a).Subperm b.primeFactorsList
    @[deprecated le_multiplicity_iff_replicate_subperm_primeFactorsList]
    theorem le_multiplicity_iff_replicate_subperm_factors {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
    n multiplicity a b (List.replicate n a).Subperm b.primeFactorsList

    Alias of le_multiplicity_iff_replicate_subperm_primeFactorsList.

    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
    @[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.