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

• padicValNat p n = if h : p ≠ 1 ∧ 0 < n then Nat.find ⋯ else 0

theorem padicValNat_def' {p n : ℕ} (hp : p ≠ 1) (hn : 0 < n) : padicValNat p n = multiplicity p n

theorem padicValNat_def {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) : padicValNat p n = multiplicity p n

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

theorem padicValNat_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) : ↑(padicValNat p n) = emultiplicity p n

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

@[simp]

theorem padicValNat.zero {p : ℕ} : padicValNat p 0 = 0

padicValNat p 0 is 0 for any p.

@[simp]

theorem padicValNat.one {p : ℕ} : padicValNat p 1 = 0

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_emultiplicity_iff_replicate_subperm_primeFactorsList {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.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