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.
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 (multiplicity p n).get ⋯ else 0
Instances For
A simplification of padicValNat
when one input is prime, by analogy with
padicValRat_def
.
Alias of le_multiplicity_iff_replicate_subperm_primeFactorsList
.
Alias of le_padicValNat_iff_replicate_subperm_primeFactorsList
.