# mathlibdocumentation

This file defines 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 ∈ ℤ}.

## 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 (prime p)] as a type class argument.

## Tags #

def padic_norm (p : ) (q : ) :

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.

Equations
Instances for padic_norm
@[protected, simp]
theorem padic_norm.eq_zpow_of_nonzero (p : ) {q : } (hq : q 0) :
q = p ^ -

Unfolds the definition of the p-adic norm of q when q ≠ 0.

@[protected]
theorem padic_norm.nonneg (p : ) (q : ) :
0 q

@[protected, simp]
theorem padic_norm.zero (p : ) :
0 = 0

The p-adic norm of 0 is 0.

@[protected, simp]
theorem padic_norm.one (p : ) :
1 = 1

The p-adic norm of 1 is 1.

p = 1 / p

The p-adic norm of p is 1/p if p > 1.

See also padic_norm.padic_norm_p_of_prime for a version that assumes p is prime.

@[simp]

The p-adic norm of p is 1/p if p is prime.

See also padic_norm.padic_norm_p for a version that assumes 1 < p.

theorem padic_norm.padic_norm_of_prime_of_ne {p q : } [p_prime : fact (nat.prime p)] [q_prime : fact (nat.prime q)] (neq : p q) :
q = 1

The p-adic norm of q is 1 if q is prime and not equal to p.

p < 1

The p-adic norm of p is less than 1 if 1 < p.

See also padic_norm.padic_norm_p_lt_one_of_prime for a version assuming prime p.

The p-adic norm of p is less than 1 if p is prime.

See also padic_norm.padic_norm_p_lt_one for a version assuming 1 < p.

@[protected]
theorem padic_norm.values_discrete (p : ) {q : } (hq : q 0) :
∃ (z : ), q = p ^ -z

padic_norm p q takes discrete values p ^ -z for z : ℤ.

@[protected, simp]
theorem padic_norm.neg (p : ) (q : ) :
(-q) = q

padic_norm p is symmetric.

@[protected]
theorem padic_norm.nonzero (p : ) [hp : fact (nat.prime p)] {q : } (hq : q 0) :
q 0

If q ≠ 0, then padic_norm p q ≠ 0.

theorem padic_norm.zero_of_padic_norm_eq_zero (p : ) [hp : fact (nat.prime p)] {q : } (h : q = 0) :
q = 0

If the p-adic norm of q is 0, then q is 0.

@[protected, simp]
theorem padic_norm.mul (p : ) [hp : fact (nat.prime p)] (q r : ) :
(q * r) = q * r

@[protected, simp]
theorem padic_norm.div (p : ) [hp : fact (nat.prime p)] (q r : ) :
(q / r) = q / r

@[protected]
theorem padic_norm.of_int (p : ) [hp : fact (nat.prime p)] (z : ) :
z 1

The p-adic norm of an integer is at most 1.

@[protected]
theorem padic_norm.nonarchimedean (p : ) [hp : fact (nat.prime p)] {q r : } :
(q + r) r)

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.

theorem padic_norm.triangle_ineq (p : ) [hp : fact (nat.prime p)] (q r : ) :
(q + r) q + r

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.

@[protected]
theorem padic_norm.sub (p : ) [hp : fact (nat.prime p)] {q r : } :
(q - r) r)

The p-adic norm of a difference is at most the max of each component. Restates the archimedean property of the p-adic norm.

theorem padic_norm.add_eq_max_of_ne (p : ) [hp : fact (nat.prime p)] {q r : } (hne : q r) :
(q + r) = r)

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.

@[protected, instance]

The p-adic norm is an absolute value: positive-definite and multiplicative, satisfying the triangle inequality.

theorem padic_norm.dvd_iff_norm_le {p : } [hp : fact (nat.prime p)] {n : } {z : } :
(p ^ n) z z p ^ -n