# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## Tags #

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 : } :
= 0

padic_val_nat p 0 is 0 for any p.

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

padic_val_nat p 1 is 0 for any p.

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

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

@[simp]
theorem padic_val_nat.eq_zero_iff {p n : } :
= 0 p = 1 n = 0 ¬p n
theorem padic_val_nat.eq_zero_of_not_dvd {p n : } (h : ¬p n) :
= 0
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) :
= z).get _
@[protected, simp]
theorem padic_val_int.zero {p : } :
= 0

padic_val_int p 0 is 0 for any p.

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

padic_val_int p 1 is 0 for any p.

@[simp]
theorem padic_val_int.of_nat {p n : } :
=

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

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

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) :
= 0
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 : ) :
(-q) =

padic_val_rat p q is symmetric in q.

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

padic_val_rat p 0 is 0 for any p.

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

padic_val_rat p 1 is 0 for any p.

@[simp]
theorem padic_val_rat.of_int {p : } {z : } :
= 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) :
= z).get _)

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) :
= q.num).get _) - ((multiplicity p q.denom).get _)
@[simp]
theorem padic_val_rat.of_nat {p n : } :
= n)

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) :
= 1

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

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

padic_val_rat coincides with padic_val_nat.

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

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) :
n) = n
@[simp]
theorem padic_val_nat_self {p : } [fact (nat.prime p)] :
= 1
theorem one_le_padic_val_nat_of_dvd {p n : } [hp : fact (nat.prime p)] (hn : 0 < n) (div : p n) :
1
theorem dvd_iff_padic_val_nat_ne_zero {p n : } [fact (nat.prime p)] (hn0 : n 0) :
p n 0
theorem padic_val_rat.finite_int_prime_iff {p : } [hp : fact (nat.prime p)] {a : } :
a 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 = d) :
= n).get _) - d).get _)

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) :
(q * r) = +

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 : } :
(q ^ k) = 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) :
(q / r) = -

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) :
(rat.mk n₁ d₁) (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 : ) :
(q + 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) :
r) (q + r)

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 < n 0 < (F i)) (hn0 : (finset.range n).sum (λ (i : ), F i) 0) :
0 < ((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)] :
a 0 b 0 (a * b) = +

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) :
(a / b) = -
@[protected]
theorem padic_val_nat.div {p b : } [hp : fact (nat.prime p)] (dvd : p b) :
(b / p) = - 1

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 ^ n) = n *

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