Vanishing of the p-adic valuation of a rational number

This file characterises when the p-adic valuation of a nonzero rational number vanishes, and compares the valuations of two rational numbers with sum 1.

Main results

• padicValRat.eq_zero_iff: a nonzero rational number has p-adic valuation zero exactly when p divides neither its numerator nor its denominator.
• padicValRat.eq_zero_of_add_eq_one_of_pos and padicValRat.eq_of_add_eq_one_of_neg: if x + y = 1, then v_p(x) > 0 forces v_p(y) = 0, and v_p(x) < 0 forces v_p(y) = v_p(x).
• padicValRat.max_natAbs_eq_of_add_eq_one: if x + y = 1, then x and y have the common denominator w = x.den, and max(|v_p(x)|, |v_p(y)|) is the largest of the valuations of the three terms of x.num + y.num = w.

theorem padicValRat.eq_zero_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} (hq : q ≠ 0) : padicValRat p q = 0 ↔ ¬p ∣ q.num.natAbs ∧ ¬p ∣ q.den

A nonzero rational number has p-adic valuation zero exactly when the prime p divides neither its numerator nor its denominator.

theorem padicValRat.eq_zero_of_add_eq_one_of_pos {p : ℕ} [Fact (Nat.Prime p)] {x y : ℚ} (hxy : x + y = 1) (hx : 0 < padicValRat p x) : padicValRat p y = 0

If x + y = 1 and x has positive p-adic valuation, then y has p-adic valuation zero.

theorem padicValRat.eq_of_add_eq_one_of_neg {p : ℕ} [Fact (Nat.Prime p)] {x y : ℚ} (hxy : x + y = 1) (hx : padicValRat p x < 0) : padicValRat p y = padicValRat p x

If x + y = 1 and x has negative p-adic valuation, then y has the same p-adic valuation as x.

theorem padicValRat.max_natAbs_eq_of_add_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℚ} (hxy : x + y = 1) : max (padicValRat p x).natAbs (padicValRat p y).natAbs = max (padicValInt p x.num) (max (padicValInt p y.num) (padicValNat p x.den))

If x + y = 1, write x = u / w and y = v / w in lowest terms, with u = x.num, v = y.num and the common denominator w = x.den, so that u + v = w. Then at every prime p the larger of |v_p(x)| and |v_p(y)| is the largest of v_p(u), v_p(v) and v_p(w).