This file defines the p-adic valuation and the p-adic norm on ℚ.
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 valuation induces a norm on ℚ. This norm is a nonarchimedean absolute value. It takes values in {0} ∪ {1/p^k | k ∈ ℤ}.
This file uses the local notation /. for rat.mk.
Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking (prime p) as a type class argument.
p-adic, p adic, padic, norm, valuation
For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number n such that p^n divides z.
padic_val_rat defines the valuation of a rational q to be the valuation of q.num minus the valuation of q.denom. If q = 0 or p = 1, then padic_val_rat p q defaults to 0.
A simplification of the definition of padic_val_rat p q when q ≠ 0 and p is prime.
padic_val_rat p q is symmetric in q.
padic_val_rat p 1 is 0 for any p.
For p ≠ 0, p ≠ 1, padic_val_rat p p` is 1.
The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.
The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.
A rewrite lemma for padic_val_rat p q when q is expressed in terms of rat.mk.
A rewrite lemma for padic_val_rat p (q * r) with conditions q ≠ 0, r ≠ 0.
A rewrite lemma for padic_val_rat p (q^k) with condition q ≠ 0`.
A rewrite lemma for padic_val_rat p (q⁻¹) with condition q ≠ 0.
A rewrite lemma for padic_val_rat p (q / r) with conditions q ≠ 0, r ≠ 0.
A condition for padic_val_rat p (n₁ / d₁) ≤ padic_val_rat 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 vlauation of q + r.
The minimum of the valuations of q and r is less than or equal to the valuation of q + r.
If q ≠ 0, the p-adic norm of a rational q is p ^ (-(padic_val_rat p q)). If q = 0, the p-adic norm of q is 0.
Unfolds the definition of the p-adic norm of q when q ≠ 0.
The p-adic norm is nonnegative.
The p-adic norm of 0 is 0.
The p-adic norm of 1 is 1.
The image of padic_norm p is {0} ∪ {p^(-n) | n ∈ ℤ}.
If q ≠ 0, then padic_norm p q ≠ 0.
padic_norm p is symmetric.
If the p-adic norm of q is 0, then q is 0.
The p-adic norm is multiplicative.
The p-adic norm respects division.
The p-adic norm of an integer is at most 1.
The p-adic norm is nonarchimedean: the norm of p + q is at most the max of the norm of p and the norm of q.
The p-adic norm respects the triangle inequality: the norm of p + q is at most the norm of p plus the norm of q.
The p-adic norm of a difference is at most the max of each component. Restates the archimedean property of the p-adic norm.
If the p-adic norms of q and r are different, then the norm of q + r is equal to the max of the norms of q and r.
The p-adic norm is an absolute value: positive-definite and multiplicative, satisfying the triangle inequality.
If p^n divides an integer z, then the p-adic norm of z is at most p^(-n).