Documentation

Mathlib.NumberTheory.Padics.PadicVal.Defs

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 Mathlib/NumberTheory/Padics/PadicNorm.lean.

source
theorem padicValNat_eq_emultiplicity_of_ne_one {p : ℕ} (hp : p ≠ 1) {n : ℕ} (hn : n ≠ 0) :
↑(padicValNat p n) = emultiplicity p n
source
@[simp]
theorem Nat.toNat_emultiplicity (p n : ℕ) :
(emultiplicity p n).toNat = padicValNat p n
source
theorem padicValNat_def' {p n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :
padicValNat p n = multiplicity p n
source
theorem padicValNat_def {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) :
padicValNat p n = multiplicity p n

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

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

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

source
@[deprecated padicValNat_eq_emultiplicity (since := "2026-03-15")]
theorem padicValNat.maxPowDiv_eq_emultiplicity {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) :
↑(padicValNat p n) = emultiplicity p n

Alias of padicValNat_eq_emultiplicity.

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

source
@[deprecated padicValNat_def' (since := "2026-03-15")]
theorem padicValNat.maxPowDiv_eq_multiplicity {p n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) :
padicValNat p n = multiplicity p n

Alias of padicValNat_def'.

source
@[deprecated padicValNat_zero_right (since := "2026-03-15")]
theorem padicValNat.zero {p : ℕ} :
padicValNat p 0 = 0
source
@[deprecated padicValNat_one_right (since := "2026-03-15")]
theorem padicValNat.one {p : ℕ} :
padicValNat p 1 = 0
source
@[simp]
theorem padicValNat.eq_zero_iff {p n : ℕ} :
padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
source
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
source
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