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.
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.
Calculations with p
-adic valuations #
padicValNat_factorial
: Legendre's Theorem. Thep
-adic valuation ofn!
is the sum of the quotientsn / p ^ i
. This sum is expressed over the finsetIco 1 b
whereb
is any bound greater thanlog p n
. SeeNat.Prime.multiplicity_factorial
for the same result but stated in the language of prime multiplicity.sub_one_mul_padicValNat_factorial
: Legendre's Theorem. Taking (p - 1
) times thep
-adic valuation ofn!
equalsn
minus the sum of basep
digits ofn
.padicValNat_choose
: Kummer's Theorem. Thep
-adic valuation ofn.choose k
is the number of carries whenk
andn - k
are added in basep
. This sum is expressed over the finsetIco 1 b
whereb
is any bound greater thanlog p n
. SeeNat.Prime.multiplicity_choose
for the same result but stated in the language of prime multiplicity.sub_one_mul_padicValNat_choose_eq_sub_sum_digits
: Kummer's Theorem. Taking (p - 1
) times thep
-adic valuation of the binomialn
overk
equals the sum of the digits ofk
plus the sum of the digits ofn - k
minus the sum of digits ofn
, all basep
.
References #
- F. Q. Gouvêa, p-adic numbers
- R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers
- https://en.wikipedia.org/wiki/P-adic_number
Tags #
p-adic, p adic, padic, norm, valuation
If p ≠ 0
and p ≠ 1
, then padicValNat p p
is 1
.
Allows for more efficient code for padicValNat
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 padicValInt p q
defaults to 0
.
Equations
- padicValInt p z = padicValNat p z.natAbs
Instances For
The p
-adic value of a natural is its p
-adic value as an integer.
If p ≠ 0
and p ≠ 1
, then padicValInt p p
is 1
.
padicValRat
defines the valuation of a rational q
to be the valuation of q.num
minus the
valuation of q.den
. If q = 0
or p = 1
, then padicValRat p q
defaults to 0
.
Equations
- padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)
Instances For
padicValRat p q
is symmetric in q
.
The p
-adic value of an integer z ≠ 0
is its p
-adic_value as a rational.
The p
-adic value of an integer z ≠ 0
is the multiplicity of p
in z
.
The p
-adic value of an integer z ≠ 0
is its p
-adic value as a rational.
If p ≠ 0
and p ≠ 1
, then padicValRat p p
is 1
.
padicValRat
coincides with padicValNat
.
The multiplicity of p : ℕ
in a : ℤ
is finite exactly when a ≠ 0
.
A rewrite lemma for padicValRat p q
when q
is expressed in terms of Rat.mk
.
A rewrite lemma for padicValRat p (q * r)
with conditions q ≠ 0
, r ≠ 0
.
A rewrite lemma for padicValRat p (q^k)
with condition q ≠ 0
.
A rewrite lemma for padicValRat p (q⁻¹)
with condition q ≠ 0
.
A rewrite lemma for padicValRat p (q / r)
with conditions q ≠ 0
, r ≠ 0
.
A condition for padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂)
, in terms of
divisibility by p^n
.
Sufficient conditions to show that the p
-adic valuation of q
is less than or equal to the
p
-adic valuation of q + r
.
The minimum of the valuations of q
and r
is at most the valuation of q + r
.
Ultrametric property of a p-adic valuation.
A finite sum of rationals with positive p
-adic valuation has positive p
-adic valuation
(if the sum is non-zero).
If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.
A rewrite lemma for padicValNat p (a * b)
with conditions a ≠ 0
, b ≠ 0
.
Dividing out by a prime factor reduces the padicValNat
by 1
.
A version of padicValRat.pow
for padicValNat
.
The p-adic valuation of n
is less than or equal to its logarithm w.r.t p
.
The p-adic valuation of n
is equal to the logarithm w.r.t p
iff
n
is less than p
raised to one plus the p-adic valuation of n
.
The p
-adic valuation of (p * n)!
is n
more than that of n!
.
The p
-adic valuation of n!
is equal to the p
-adic valuation of the factorial of the
largest multiple of p
below n
, i.e. (p * ⌊n / p⌋)!
.
Legendre's Theorem
The p
-adic valuation of n!
is the sum of the quotients n / p ^ i
. This sum is expressed
over the finset Ico 1 b
where b
is any bound greater than log p n
.
Kummer's Theorem
The p
-adic valuation of n.choose k
is the number of carries when k
and n - k
are added
in base p
. This sum is expressed over the finset Ico 1 b
where b
is any bound greater than
log p n
.
Kummer's Theorem
The p
-adic valuation of (n + k).choose k
is the number of carries when k
and n
are added
in base p
. This sum is expressed over the finset Ico 1 b
where b
is any bound greater than
log p (n + k)
.
Kummer's Theorem
Taking (p - 1
) times the p
-adic valuation of the binomial n + k
over k
equals the sum of the
digits of k
plus the sum of the digits of n
minus the sum of digits of n + k
, all base p
.
Kummer's Theorem
Taking (p - 1
) times the p
-adic valuation of the binomial n
over k
equals the sum of the
digits of k
plus the sum of the digits of n - k
minus the sum of digits of n
, all base p
.