mathlib documentation

number_theory.padics.padic_val

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 padic_norm.lean.

Notations #

This file uses the local notation /. for rat.mk.

Implementation notes #

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [fact p.prime] as a type class argument.

References #

Tags #

p-adic, p adic, padic, norm, valuation

def padic_val_nat (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 z. If n = 0 or p = 1, then padic_val_nat p q defaults to 0.

Equations
@[protected, simp]
theorem padic_val_nat.zero {p : } :

padic_val_nat p 0 is 0 for any p.

@[protected, simp]
theorem padic_val_nat.one {p : } :

padic_val_nat p 1 is 0 for any p.

@[simp]
theorem padic_val_nat.self {p : } (hp : 1 < p) :

If p ≠ 0 and p ≠ 1, then padic_val_rat p p is 1.

theorem padic_val_nat.eq_zero_of_not_dvd {p n : } (h : ¬p n) :
def padic_val_int (p : ) (z : ) :

For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number k such that p^k divides z. If x = 0 or p = 1, then padic_val_int p q defaults to 0.

Equations
theorem padic_val_int.of_ne_one_ne_zero {p : } {z : } (hp : p 1) (hz : z 0) :
@[protected, simp]
theorem padic_val_int.zero {p : } :

padic_val_int p 0 is 0 for any p.

@[protected, simp]
theorem padic_val_int.one {p : } :

padic_val_int p 1 is 0 for any p.

@[simp]

The p-adic value of a natural is its p-adic value as an integer.

theorem padic_val_int.self {p : } (hp : 1 < p) :

If p ≠ 0 and p ≠ 1, then padic_val_int p p is 1.

theorem padic_val_int.eq_zero_of_not_dvd {p : } {z : } (h : ¬p z) :
def padic_val_rat (p : ) (q : ) :

padic_val_rat defines the valuation of a rational q to be the valuation of q.num minus the valuation of q.denom. If q = 0 or p = 1, then padic_val_rat p q defaults to 0.

Equations
@[protected, simp]
theorem padic_val_rat.neg {p : } (q : ) :

padic_val_rat p q is symmetric in q.

@[protected, simp]
theorem padic_val_rat.zero {p : } :

padic_val_rat p 0 is 0 for any p.

@[protected, simp]
theorem padic_val_rat.one {p : } :

padic_val_rat p 1 is 0 for any p.

@[simp]
theorem padic_val_rat.of_int {p : } {z : } :

The p-adic value of an integer z ≠ 0 is its p-adic_value as a rational.

theorem padic_val_rat.of_int_multiplicity {p : } {z : } (hp : p 1) (hz : z 0) :

The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.

theorem padic_val_rat.multiplicity_sub_multiplicity {p : } {q : } (hp : p 1) (hq : q 0) :
@[simp]

The p-adic value of an integer z ≠ 0 is its p-adic value as a rational.

theorem padic_val_rat.self {p : } (hp : 1 < p) :

If p ≠ 0 and p ≠ 1, then padic_val_rat p p is 1.

@[norm_cast]
theorem padic_val_rat_of_nat {p : } (n : ) :

padic_val_rat coincides with padic_val_nat.

theorem padic_val_nat_def {p : } [hp : fact (nat.prime p)] {n : } (hn : 0 < n) :

A simplification of padic_val_nat when one input is prime, by analogy with padic_val_rat_def.

theorem padic_val_nat_def' {p n : } (hp : p 1) (hn : 0 < n) :
@[simp]
theorem padic_val_nat_self {p : } [fact (nat.prime p)] :
theorem one_le_padic_val_nat_of_dvd {p n : } [hp : fact (nat.prime p)] (hn : 0 < n) (div : p n) :
theorem dvd_iff_padic_val_nat_ne_zero {p n : } [fact (nat.prime p)] (hn0 : n 0) :

The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.

@[protected]
theorem padic_val_rat.defn (p : ) [hp : fact (nat.prime p)] {q : } {n d : } (hqz : q 0) (qdf : q = rat.mk n d) :

A rewrite lemma for padic_val_rat p q when q is expressed in terms of rat.mk.

@[protected]
theorem padic_val_rat.mul {p : } [hp : fact (nat.prime p)] {q r : } (hq : q 0) (hr : r 0) :

A rewrite lemma for padic_val_rat p (q * r) with conditions q ≠ 0, r ≠ 0.

@[protected]
theorem padic_val_rat.pow {p : } [hp : fact (nat.prime p)] {q : } (hq : q 0) {k : } :

A rewrite lemma for padic_val_rat p (q^k) with condition q ≠ 0.

@[protected]
theorem padic_val_rat.inv {p : } [hp : fact (nat.prime p)] (q : ) :

A rewrite lemma for padic_val_rat p (q⁻¹) with condition q ≠ 0.

@[protected]
theorem padic_val_rat.div {p : } [hp : fact (nat.prime p)] {q r : } (hq : q 0) (hr : r 0) :

A rewrite lemma for padic_val_rat p (q / r) with conditions q ≠ 0, r ≠ 0.

theorem padic_val_rat.padic_val_rat_le_padic_val_rat_iff {p : } [hp : fact (nat.prime p)] {n₁ n₂ d₁ d₂ : } (hn₁ : n₁ 0) (hn₂ : n₂ 0) (hd₁ : d₁ 0) (hd₂ : d₂ 0) :
padic_val_rat p (rat.mk n₁ d₁) padic_val_rat p (rat.mk n₂ d₂) ∀ (n : ), p ^ n n₁ * d₂p ^ n n₂ * d₁

A condition for padic_val_rat p (n₁ / d₁) ≤ padic_val_rat p (n₂ / d₂), in terms of divisibility by p^n.

theorem padic_val_rat.le_padic_val_rat_add_of_le {p : } [hp : fact (nat.prime p)] {q r : } (hqr : q + r 0) (h : padic_val_rat p q padic_val_rat p r) :

Sufficient conditions to show that the p-adic valuation of q is less than or equal to the p-adic valuation of q + r.

theorem padic_val_rat.min_le_padic_val_rat_add {p : } [hp : fact (nat.prime p)] {q r : } (hqr : q + r 0) :

The minimum of the valuations of q and r is at most the valuation of q + r.

theorem padic_val_rat.sum_pos_of_pos {p : } [hp : fact (nat.prime p)] {n : } {F : } (hF : ∀ (i : ), i < n0 < padic_val_rat p (F i)) (hn0 : (finset.range n).sum (λ (i : ), F i) 0) :
0 < padic_val_rat p ((finset.range n).sum (λ (i : ), F i))

A finite sum of rationals with positive p-adic valuation has positive p-adic valuation (if the sum is non-zero).

@[protected]
theorem padic_val_nat.mul {p a b : } [hp : fact (nat.prime p)] (ha : a 0) (hb : b 0) :

A rewrite lemma for padic_val_nat p (a * b) with conditions a ≠ 0, b ≠ 0.

@[protected]
theorem padic_val_nat.div_of_dvd {p a b : } [hp : fact (nat.prime p)] (h : b a) :
@[protected]
theorem padic_val_nat.div {p b : } [hp : fact (nat.prime p)] (dvd : p b) :

Dividing out by a prime factor reduces the padic_val_nat by 1.

@[protected]
theorem padic_val_nat.pow {p a : } [hp : fact (nat.prime p)] (n : ) (ha : a 0) :

A version of padic_val_rat.pow for padic_val_nat.

@[protected, simp]
theorem padic_val_nat.prime_pow {p : } [hp : fact (nat.prime p)] (n : ) :
padic_val_nat p (p ^ n) = n
@[protected]
theorem padic_val_nat.div_pow {p a b : } [hp : fact (nat.prime p)] (dvd : p ^ a b) :
padic_val_nat p (b / p ^ a) = padic_val_nat p b - a
theorem dvd_of_one_le_padic_val_nat {p n : } (hp : 1 padic_val_nat p n) :
p n
theorem pow_padic_val_nat_dvd {p n : } :
theorem pow_succ_padic_val_nat_not_dvd {p n : } [hp : fact (nat.prime p)] (hn : 0 < n) :
¬p ^ (padic_val_nat p n + 1) n
theorem padic_val_nat_dvd_iff {p : } (n : ) [hp : fact (nat.prime p)] (a : ) :
p ^ n a a = 0 n padic_val_nat p a
theorem padic_val_nat_primes {p q : } [hp : fact (nat.prime p)] [hq : fact (nat.prime q)] (neq : p q) :
@[protected]
theorem padic_val_nat.div' {p : } [hp : fact (nat.prime p)] {m : } (cpm : p.coprime m) {b : } (dvd : m b) :
theorem range_pow_padic_val_nat_subset_divisors' {p n : } [hp : fact (nat.prime p)] :
finset.image (λ (t : ), p ^ (t + 1)) (finset.range (padic_val_nat p n)) n.divisors \ {1}
theorem padic_val_int_dvd_iff {p : } [hp : fact (nat.prime p)] (n : ) (a : ) :
p ^ n a a = 0 n padic_val_int p a
theorem padic_val_int_dvd {p : } [hp : fact (nat.prime p)] (a : ) :
theorem padic_val_int_self {p : } [hp : fact (nat.prime p)] :
theorem padic_val_int.mul {p : } [hp : fact (nat.prime p)] {a b : } (ha : a 0) (hb : b 0) :
theorem padic_val_int_mul_eq_succ {p : } [hp : fact (nat.prime p)] (a : ) (ha : a 0) :