Mathlib.NumberTheory.Padics.PadicVal.Defs

Module docstring

{"# 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. "}

padicValNat definition

(p : ℕ) (n : ℕ) : ℕ

Full source

/-- 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`. -/
def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
  if h : p ≠ 1 ∧ 0 < n then Nat.find (finiteMultiplicity_iff.2 h) else 0

$ p $-adic valuation on natural numbers

Informal description

For a natural number $ p \neq 1 $ and a nonzero natural number $ n $, the $ p $-adic valuation of $ n $, denoted $ \text{padicValNat}(p, n) $, is the largest natural number $ k $ such that $ p^k $ divides $ n $. If $ p = 1 $ or $ n = 0 $, the $ p $-adic valuation is defined to be $ 0 $.

padicValNat_def' theorem

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

Full source

theorem padicValNat_def' {n : ℕ} (hp : p ≠ 1) (hn : 0 < n) :
    padicValNat p n = multiplicity p n := by
  simp [padicValNat, hp, hn, multiplicity, emultiplicity, finiteMultiplicity_iff.2 ⟨hp, hn⟩]
  convert (WithTop.untopD_coe ..).symm

$p$-adic Valuation Equals Multiplicity for $p \neq 1$ and $n > 0$

Informal description

For a natural number $p \neq 1$ and a positive natural number $n$, the $p$-adic valuation of $n$ equals the multiplicity of $p$ in $n$, i.e., $\text{padicValNat}(p, n) = \text{multiplicity}(p, n)$.

padicValNat_def theorem

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

Full source

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_def [hp : Fact p.Prime] {n : ℕ} (hn : 0 < n) :
    padicValNat p n = multiplicity p n :=
  padicValNat_def' hp.out.ne_one hn

$p$-adic Valuation Equals Multiplicity for Prime $p$ and Positive $n$

Informal description

For a prime natural number $p$ and a positive natural number $n$, the $p$-adic valuation of $n$ equals the multiplicity of $p$ in $n$, i.e., $\text{padicValNat}(p, n) = \text{multiplicity}(p, n)$.

padicValNat_eq_emultiplicity theorem

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

Full source

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_eq_emultiplicity [hp : Fact p.Prime] {n : ℕ} (hn : 0 < n) :
    padicValNat p n = emultiplicity p n := by
  rw [(finiteMultiplicity_iff.2 ⟨hp.out.ne_one, hn⟩).emultiplicity_eq_multiplicity]
  exact_mod_cast padicValNat_def hn

$p$-adic Valuation Equals Extended Multiplicity for Prime $p$ and Positive $n$

Informal description

For a prime natural number $p$ and a positive natural number $n$, the $p$-adic valuation of $n$ equals the extended multiplicity of $p$ in $n$, i.e., $\text{padicValNat}(p, n) = \text{emultiplicity}(p, n)$.

padicValNat.zero theorem

: padicValNat p 0 = 0

Full source

/-- `padicValNat p 0` is `0` for any `p`. -/
@[simp]
protected theorem zero : padicValNat p 0 = 0 := by simp [padicValNat]

$p$-adic valuation of zero is zero

Informal description

For any natural number $p$, the $p$-adic valuation of $0$ is $0$, i.e., $\text{padicValNat}(p, 0) = 0$.

padicValNat.one theorem

: padicValNat p 1 = 0

Full source

/-- `padicValNat p 1` is `0` for any `p`. -/
@[simp]
protected theorem one : padicValNat p 1 = 0 := by simp [padicValNat]

$p$-adic valuation of 1 is zero

Informal description

For any natural number $p$, the $p$-adic valuation of $1$ is $0$, i.e., $\text{padicValNat}(p, 1) = 0$.

le_emultiplicity_iff_replicate_subperm_primeFactorsList theorem

 {a b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList

Full source

theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime)
    (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList :=
  (replicate_subperm_primeFactorsList_iff ha hb).trans
    pow_dvd_iff_le_emultiplicity |>.symm

Extended Multiplicity Bound via Prime Factors Subpermutation

Informal description

For a prime natural number $a$, a nonzero natural number $b$, and a natural number $n$, the extended multiplicity of $a$ in $b$ is at least $n$ if and only if the list consisting of $n$ copies of $a$ is a subpermutation of the prime factors list of $b$. In other words, $n \leq \text{emultiplicity}\, a\, b$ if and only if $\text{replicate}\, n\, a$ is a subpermutation of $\text{primeFactorsList}\, b$.

le_padicValNat_iff_replicate_subperm_primeFactorsList theorem

{a b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) : n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Full source

theorem le_padicValNat_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime)
    (hb : b ≠ 0) :
    n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList := by
  rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity,     ← padicValNat_def' ha.ne_one (Nat.pos_of_ne_zero hb),
    Nat.cast_le]

$p$-adic Valuation Bound via Prime Factors Subpermutation: $n \leq \text{padicValNat}(a, b) \leftrightarrow \text{replicate}(n, a) \lesssim \text{primeFactorsList}(b)$

Informal description

For a prime natural number $a$, a nonzero natural number $b$, and a natural number $n$, the $p$-adic valuation of $b$ is at least $n$ if and only if the list consisting of $n$ copies of $a$ is a subpermutation of the prime factors list of $b$. In other words, $n \leq \text{padicValNat}(a, b)$ if and only if $\text{replicate}(n, a)$ is a subpermutation of $\text{primeFactorsList}(b)$.