# 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.

## 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.

## Calculations with p-adic valuations #

• padicValNat_factorial: Legendre's Theorem. The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n. See Nat.Prime.multiplicity_factorial for the same result but stated in the language of prime multiplicity.

• sub_one_mul_padicValNat_factorial: Legendre's Theorem. Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

• padicValNat_choose: Kummer's Theorem. The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n. See Nat.Prime.multiplicity_choose for the same result but stated in the language of prime multiplicity.

• sub_one_mul_padicValNat_choose_eq_sub_sum_digits: Kummer's Theorem. Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

## Tags #

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
@[simp]
theorem padicValNat.zero {p : } :
= 0

padicValNat p 0 is 0 for any p.

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

padicValNat p 1 is 0 for any p.

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

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

@[simp]
theorem padicValNat.eq_zero_iff {p : } {n : } :
= 0 p = 1 n = 0 ¬p n
theorem padicValNat.eq_zero_of_not_dvd {p : } {n : } (h : ¬p n) :
= 0
theorem padicValNat.maxPowDiv_eq_multiplicity {p : } {n : } (hp : 1 < p) (hn : 0 < n) :
(p.maxPowDiv n) =
theorem padicValNat.maxPowDiv_eq_multiplicity_get {p : } {n : } (hp : 1 < p) (hn : 0 < n) (h : ) :
p.maxPowDiv n = (multiplicity p n).get h
@[csimp]

Allows for more efficient code for padicValNat

def padicValInt (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 padicValInt p q defaults to 0.

Equations
Instances For
theorem padicValInt.of_ne_one_ne_zero {p : } {z : } (hp : p 1) (hz : z 0) :
= (multiplicity (↑p) z).get
@[simp]
theorem padicValInt.zero {p : } :
= 0

padicValInt p 0 is 0 for any p.

@[simp]
theorem padicValInt.one {p : } :
= 0

padicValInt p 1 is 0 for any p.

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

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

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

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

theorem padicValInt.eq_zero_of_not_dvd {p : } {z : } (h : ¬p z) :
= 0
def padicValRat (p : ) (q : ) :

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

Equations
Instances For
theorem padicValRat_def (p : ) (q : ) :
@[simp]
theorem padicValRat.neg {p : } (q : ) :

padicValRat p q is symmetric in q.

@[simp]
theorem padicValRat.zero {p : } :
= 0

padicValRat p 0 is 0 for any p.

@[simp]
theorem padicValRat.one {p : } :
= 0

padicValRat p 1 is 0 for any p.

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

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

theorem padicValRat.of_int_multiplicity {p : } {z : } (hp : p 1) (hz : z 0) :
padicValRat p z = ((multiplicity (↑p) z).get )

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

theorem padicValRat.multiplicity_sub_multiplicity {p : } {q : } (hp : p 1) (hq : q 0) :
= ((multiplicity (↑p) q.num).get ) - ((multiplicity p q.den).get )
@[simp]
theorem padicValRat.of_nat {p : } {n : } :

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

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

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

theorem padicValRat_of_nat {p : } (n : ) :

padicValRat coincides with padicValNat.

theorem padicValNat_def {p : } [hp : Fact (Nat.Prime p)] {n : } (hn : 0 < 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_self {p : } [Fact (Nat.Prime p)] :
= 1
theorem one_le_padicValNat_of_dvd {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : 0 < n) (div : p n) :
1
theorem dvd_iff_padicValNat_ne_zero {p : } {n : } [Fact (Nat.Prime p)] (hn0 : n 0) :
p n 0
theorem le_multiplicity_iff_replicate_subperm_primeFactorsList {a : } {b : } {n : } (ha : ) (hb : b 0) :
n (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 : ) (hb : b 0) :
n (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 : ) (hb : b 0) :
n (List.replicate n a).Subperm b.primeFactorsList
theorem le_padicValNat_iff_replicate_subperm_factors {a : } {b : } {n : } (ha : ) (hb : b 0) :
n (List.replicate n a).Subperm b.primeFactorsList

Alias of le_padicValNat_iff_replicate_subperm_primeFactorsList.

theorem padicValRat.finite_int_prime_iff {p : } [hp : Fact (Nat.Prime p)] {a : } :

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

theorem padicValRat.defn (p : ) [hp : Fact (Nat.Prime p)] {q : } {n : } {d : } (hqz : q 0) (qdf : q = ) :
= ((multiplicity (↑p) n).get ) - ((multiplicity (↑p) d).get )

A rewrite lemma for padicValRat p q when q is expressed in terms of Rat.mk.

theorem padicValRat.mul {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hq : q 0) (hr : r 0) :
padicValRat p (q * r) = +

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

theorem padicValRat.pow {p : } [hp : Fact (Nat.Prime p)] {q : } (hq : q 0) {k : } :
padicValRat p (q ^ k) = k *

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

theorem padicValRat.inv {p : } [hp : Fact (Nat.Prime p)] (q : ) :
= -

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

theorem padicValRat.div {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hq : q 0) (hr : r 0) :
padicValRat p (q / r) = -

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

theorem padicValRat.padicValRat_le_padicValRat_iff {p : } [hp : Fact (Nat.Prime p)] {n₁ : } {n₂ : } {d₁ : } {d₂ : } (hn₁ : n₁ 0) (hn₂ : n₂ 0) (hd₁ : d₁ 0) (hd₂ : d₂ 0) :
padicValRat p (Rat.divInt n₁ d₁) padicValRat p (Rat.divInt n₂ d₂) ∀ (n : ), p ^ n n₁ * d₂p ^ n n₂ * d₁

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

theorem padicValRat.le_padicValRat_add_of_le {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (h : ) :

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 padicValRat.min_le_padicValRat_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 padicValRat.add_eq_min {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (hq : q 0) (hr : r 0) (hval : ) :

Ultrametric property of a p-adic valuation.

theorem padicValRat.add_eq_of_lt {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (hq : q 0) (hr : r 0) (hval : < ) :
padicValRat p (q + r) =
theorem padicValRat.lt_add_of_lt {p : } [hp : Fact (Nat.Prime p)] {q : } {r₁ : } {r₂ : } (hqr : r₁ + r₂ 0) (hval₁ : < padicValRat p r₁) (hval₂ : < padicValRat p r₂) :
< padicValRat p (r₁ + r₂)
@[simp]
theorem padicValRat.self_pow_inv {p : } [hp : Fact (Nat.Prime p)] (r : ) :
padicValRat p (p ^ r)⁻¹ = -r
theorem padicValRat.sum_pos_of_pos {p : } [hp : Fact (Nat.Prime p)] {n : } {F : } (hF : i < n, 0 < padicValRat p (F i)) (hn0 : i, F i 0) :
0 < padicValRat p (∑ i, F i)

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

theorem padicValRat.lt_sum_of_lt {p : } {j : } [hp : Fact (Nat.Prime p)] {F : } {S : } (hS : S.Nonempty) (hF : iS, padicValRat p (F j) < padicValRat p (F i)) (hn1 : ∀ (i : ), 0 < F i) :

If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.

theorem padicValNat.mul {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] :
a 0b 0padicValNat p (a * b) = +

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

theorem padicValNat.div_of_dvd {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] (h : b a) :
padicValNat p (a / b) = -
theorem padicValNat.div {p : } {b : } [hp : Fact (Nat.Prime p)] (dvd : p b) :
padicValNat p (b / p) = - 1

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

theorem padicValNat.pow {p : } {a : } [hp : Fact (Nat.Prime p)] (n : ) (ha : a 0) :
padicValNat p (a ^ n) = n *

A version of padicValRat.pow for padicValNat.

@[simp]
theorem padicValNat.prime_pow {p : } [hp : Fact (Nat.Prime p)] (n : ) :
padicValNat p (p ^ n) = n
theorem padicValNat.div_pow {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] (dvd : p ^ a b) :
padicValNat p (b / p ^ a) = - a
theorem padicValNat.div' {p : } [hp : Fact (Nat.Prime p)] {m : } (cpm : p.Coprime m) {b : } (dvd : m b) :
padicValNat p (b / m) =
theorem dvd_of_one_le_padicValNat {p : } {n : } (hp : 1 ) :
p n
theorem pow_padicValNat_dvd {p : } {n : } :
p ^ n
theorem padicValNat_dvd_iff_le {p : } [hp : Fact (Nat.Prime p)] {a : } {n : } (ha : a 0) :
p ^ n a n
theorem padicValNat_dvd_iff {p : } (n : ) [hp : Fact (Nat.Prime p)] (a : ) :
p ^ n a a = 0 n
theorem pow_succ_padicValNat_not_dvd {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : n 0) :
¬p ^ ( + 1) n
theorem padicValNat_primes {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (neq : p q) :
= 0
theorem padicValNat_prime_prime_pow {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (neq : p q) :
padicValNat p (q ^ n) = 0
theorem padicValNat_mul_pow_left {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (m : ) (neq : p q) :
padicValNat p (p ^ n * q ^ m) = n
theorem padicValNat_mul_pow_right {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (m : ) (neq : q p) :
padicValNat q (p ^ n * q ^ m) = m
theorem padicValNat_le_nat_log {p : } (n : ) :

The p-adic valuation of n is less than or equal to its logarithm w.r.t p.

theorem nat_log_eq_padicValNat_iff {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : 0 < n) :
Nat.log p n = n < p ^ ( + 1)

The p-adic valuation of n is equal to the logarithm w.r.t p iff n is less than p raised to one plus the p-adic valuation of n.

theorem Nat.log_ne_padicValNat_succ {n : } (hn : n 0) :
Nat.log 2 n padicValNat 2 (n + 1)
theorem range_pow_padicValNat_subset_divisors {p : } {n : } (hn : n 0) :
Finset.image (fun (x : ) => p ^ x) (Finset.range ( + 1)) n.divisors
theorem range_pow_padicValNat_subset_divisors' {p : } {n : } [hp : Fact (Nat.Prime p)] :
Finset.image (fun (t : ) => p ^ (t + 1)) (Finset.range (padicValNat p n)) n.divisors.erase 1
theorem padicValNat_factorial_mul {p : } (n : ) [hp : Fact (Nat.Prime p)] :

The p-adic valuation of (p * n)! is n more than that of n!.

theorem padicValNat_eq_zero_of_mem_Ioo {p : } {m : } {k : } (hm : m Set.Ioo (p * k) (p * (k + 1))) :
= 0

The p-adic valuation of m equals zero if it is between p * k and p * (k + 1) for some k.

theorem padicValNat_factorial_mul_add {p : } {n : } (m : ) [hp : Fact (Nat.Prime p)] (h : n < p) :
padicValNat p (p * m + n).factorial = padicValNat p (p * m).factorial
@[simp]
theorem padicValNat_mul_div_factorial {p : } (n : ) [hp : Fact (Nat.Prime p)] :

The p-adic valuation of n! is equal to the p-adic valuation of the factorial of the largest multiple of p below n, i.e. (p * ⌊n / p⌋)!.

theorem padicValNat_factorial {p : } {n : } {b : } [hp : Fact (Nat.Prime p)] (hnb : Nat.log p n < b) :
padicValNat p n.factorial = i, n / p ^ i

Legendre's Theorem

The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem sub_one_mul_padicValNat_factorial {p : } [hp : Fact (Nat.Prime p)] (n : ) :
(p - 1) * padicValNat p n.factorial = n - (p.digits n).sum

Legendre's Theorem

Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

theorem padicValNat_choose {p : } {n : } {k : } {b : } [hp : Fact (Nat.Prime p)] (hkn : k n) (hnb : Nat.log p n < b) :
padicValNat p (n.choose k) = (Finset.filter (fun (i : ) => p ^ i k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card

Kummer's Theorem

The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem padicValNat_choose' {p : } {n : } {k : } {b : } [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) :
padicValNat p ((n + k).choose k) = (Finset.filter (fun (i : ) => p ^ i k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card

Kummer's Theorem

The p-adic valuation of (n + k).choose k is the number of carries when k and n are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p (n + k).

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {p : } {k : } {n : } [hp : Fact (Nat.Prime p)] :
(p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n + k over k equals the sum of the digits of k plus the sum of the digits of n minus the sum of digits of n + k, all base p.

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {p : } {k : } {n : } [hp : Fact (Nat.Prime p)] (h : k n) :
(p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

theorem padicValInt_dvd_iff {p : } [hp : Fact (Nat.Prime p)] (n : ) (a : ) :
p ^ n a a = 0 n
theorem padicValInt_dvd {p : } [hp : Fact (Nat.Prime p)] (a : ) :
p ^ a
theorem padicValInt_self {p : } [hp : Fact (Nat.Prime p)] :