scilib documentation

number_theory.padics.padic_val

p-adic Valuation #

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.

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

padic_val_nat p n = dite (p ≠ 1 ∧ 0 < n) (λ (h : p ≠ 1 ∧ 0 < n), (multiplicity p n).get _) (λ (h : ¬(p ≠ 1 ∧ 0 < n)), 0)

@[protected, simp]

theorem padic_val_nat.zero {p : ℕ} :

padic_val_nat p 0 = 0

padic_val_nat p 0 is 0 for any p.

@[protected, simp]

theorem padic_val_nat.one {p : ℕ} :

padic_val_nat p 1 = 0

padic_val_nat p 1 is 0 for any p.

@[simp]

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

padic_val_nat p 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 : ℕ} :

padic_val_nat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

theorem padic_val_nat.eq_zero_of_not_dvd {p n : ℕ} (h : ¬p ∣ n) :

padic_val_nat 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

padic_val_int p z = padic_val_nat p z.nat_abs

theorem padic_val_int.of_ne_one_ne_zero {p : ℕ} {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) :

padic_val_int p z = (multiplicity ↑p z).get _

@[protected, simp]

theorem padic_val_int.zero {p : ℕ} :

padic_val_int p 0 = 0

padic_val_int p 0 is 0 for any p.

@[protected, simp]

theorem padic_val_int.one {p : ℕ} :

padic_val_int p 1 = 0

padic_val_int p 1 is 0 for any p.

@[simp]

theorem padic_val_int.of_nat {p n : ℕ} :

padic_val_int p ↑n = padic_val_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) :

padic_val_int p ↑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) :

padic_val_int 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

padic_val_rat p q = ↑(padic_val_int p q.num) - ↑(padic_val_nat p q.denom)

@[protected, simp]

theorem padic_val_rat.neg {p : ℕ} (q : ℚ) :

padic_val_rat p (-q) = padic_val_rat p q

padic_val_rat p q is symmetric in q.

@[protected, simp]

theorem padic_val_rat.zero {p : ℕ} :

padic_val_rat p 0 = 0

padic_val_rat p 0 is 0 for any p.

@[protected, simp]

theorem padic_val_rat.one {p : ℕ} :

padic_val_rat p 1 = 0

padic_val_rat p 1 is 0 for any p.

@[simp]

theorem padic_val_rat.of_int {p : ℕ} {z : ℤ} :

padic_val_rat p ↑z = ↑(padic_val_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) :

padic_val_rat p ↑z = ↑((multiplicity ↑p 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) :

padic_val_rat p q = ↑((multiplicity ↑p q.num).get _) - ↑((multiplicity p q.denom).get _)

@[simp]

theorem padic_val_rat.of_nat {p n : ℕ} :

padic_val_rat p ↑n = ↑(padic_val_nat p 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) :

padic_val_rat p ↑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 ≤ padic_val_rat p ↑n

@[norm_cast]

theorem padic_val_rat_of_nat {p : ℕ} (n : ℕ) :

↑(padic_val_nat p n) = padic_val_rat 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) :

padic_val_nat p n = (multiplicity p 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) :

↑(padic_val_nat p n) = multiplicity p n

@[simp]

theorem padic_val_nat_self {p : ℕ} [fact (nat.prime p)] :

padic_val_nat p p = 1

theorem one_le_padic_val_nat_of_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn : 0 < n) (div : p ∣ n) :

1 ≤ padic_val_nat p n

theorem dvd_iff_padic_val_nat_ne_zero {p n : ℕ} [fact (nat.prime p)] (hn0 : n ≠ 0) :

p ∣ n ↔ padic_val_nat p n ≠ 0

theorem padic_val_rat.finite_int_prime_iff {p : ℕ} [hp : fact (nat.prime p)] {a : ℤ} :

multiplicity.finite ↑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 = rat.mk n d) :

padic_val_rat p q = ↑((multiplicity ↑p n).get _) - ↑((multiplicity ↑p 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) :

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

padic_val_rat p (q ^ k) = ↑k * padic_val_rat p q

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 : ℚ) :

padic_val_rat p q⁻¹ = -padic_val_rat 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) :

padic_val_rat p (q / r) = padic_val_rat p q - padic_val_rat p 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) :

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

padic_val_rat p q ≤ padic_val_rat p (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) :

linear_order.min (padic_val_rat p q) (padic_val_rat p r) ≤ padic_val_rat p (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 < 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)] :

a ≠ 0 → b ≠ 0 → padic_val_nat p (a * b) = padic_val_nat p a + padic_val_nat p 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) :

padic_val_nat p (a / b) = padic_val_nat p a - padic_val_nat p b

@[protected]

theorem padic_val_nat.div {p b : ℕ} [hp : fact (nat.prime p)] (dvd : p ∣ b) :

padic_val_nat p (b / p) = padic_val_nat p b - 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) :

padic_val_nat p (a ^ n) = n * padic_val_nat p a

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

@[protected]

theorem padic_val_nat.div' {p : ℕ} [hp : fact (nat.prime p)] {m : ℕ} (cpm : p.coprime m) {b : ℕ} (dvd : m ∣ b) :

padic_val_nat p (b / m) = padic_val_nat p b

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 : ℕ} :

p ^ padic_val_nat p n ∣ n

theorem padic_val_nat_dvd_iff_le {p : ℕ} [hp : fact (nat.prime p)] {a n : ℕ} (ha : a ≠ 0) :

p ^ n ∣ a ↔ n ≤ padic_val_nat p a

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 pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn : n ≠ 0) :

¬p ^ (padic_val_nat p n + 1) ∣ n

theorem padic_val_nat_primes {p q : ℕ} [hp : fact (nat.prime p)] [hq : fact (nat.prime q)] (neq : p ≠ q) :

padic_val_nat p q = 0

theorem range_pow_padic_val_nat_subset_divisors {p n : ℕ} (hn : n ≠ 0) :

finset.image (has_pow.pow p) (finset.range (padic_val_nat p n + 1)) ⊆ n.divisors

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.erase 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 : ℤ) :

↑p ^ padic_val_int p a ∣ a

theorem padic_val_int_self {p : ℕ} [hp : fact (nat.prime p)] :

padic_val_int p ↑p = 1

theorem padic_val_int.mul {p : ℕ} [hp : fact (nat.prime p)] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :

padic_val_int p (a * b) = padic_val_int p a + padic_val_int p b

theorem padic_val_int_mul_eq_succ {p : ℕ} [hp : fact (nat.prime p)] (a : ℤ) (ha : a ≠ 0) :

padic_val_int p (a * ↑p) = padic_val_int p a + 1