Rational numbers at almost every prime

A rational number has only finitely many primes dividing its numerator or its denominator. Hence its image in ℚ_[p] is a p-adic integer at all but finitely many primes p, and a nonzero rational number is a p-adic unit at all but finitely many primes. These are the statements that make a rational object, such as a rational basis or a rational isometry, integral in every completion outside a finite set of primes. Conversely, a rational number that is a p-adic integer at every prime is an integer, and so is a rational number whose denominator is a power of p and which is a p-adic integer. Consequently two rational numbers agree in ℚ/ℤ when their difference has p-power denominator and is a p-adic integer.

Main results

• Rat.eventually_not_dvd_den: almost every prime is coprime to the denominator.
• Padic.eventually_norm_rat_le_one: a rational number is p-adically integral at almost every prime.
• Padic.eventually_norm_rat_eq_one: a nonzero rational number has p-adic norm one at almost every prime.
• Padic.forall_norm_rat_le_one_iff_den_eq_one: a rational number is an integer exactly when it is a p-adic integer at every prime.
• Padic.den_eq_one_of_pow_mul_eq_of_norm_rat_le_one: a p-adic integer whose product with a power of p is an integer is an integer.
• Padic.addCircle_coe_eq_coe_of_eq_add_algebraMap: two rational numbers agree in ℚ/ℤ when their difference has p-power denominator and lies in ℤ_p.

theorem Rat.eventually_not_dvd_den (q : ℚ) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ¬↑p ∣ q.den

All but finitely many primes do not divide the denominator of a rational number.

theorem Padic.eventually_norm_rat_le_one (q : ℚ) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ‖↑q‖ ≤ 1

A rational number is a p-adic integer at all but finitely many primes p.

theorem Padic.eventually_norm_rat_eq_one {q : ℚ} (hq : q ≠ 0) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ‖↑q‖ = 1

A nonzero rational number is a p-adic unit at all but finitely many primes p.

theorem Padic.forall_norm_rat_le_one_iff_den_eq_one {q : ℚ} : (∀ (p : Nat.Primes), ‖↑q‖ ≤ 1) ↔ q.den = 1

A rational number is an integer, that is, has denominator one, exactly when it is a p-adic integer at every prime p.

theorem Padic.den_eq_one_of_pow_mul_eq_of_norm_rat_le_one {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ} {k : ℕ} {n : ℤ} (hn : ↑p ^ k * q = ↑n) (hq : ‖↑q‖ ≤ 1) : q.den = 1

A rational number q such that p ^ k * q is an integer is itself an integer as soon as it is a p-adic integer.

theorem Padic.addCircle_coe_eq_coe_of_eq_add_algebraMap {p : ℕ} [Fact (Nat.Prime p)] {r s : ℚ} {k : ℕ} {n : ℤ} (hn : ↑p ^ k * (r - s) = ↑n) {z : ℤ_[p]} (hz : ↑r = ↑s + (algebraMap ℤ_[p] ℚ_[p]) z) : ↑r = ↑s

Two rational numbers agree modulo ℤ when their difference has p-power denominator and lies in ℤ_p.

theorem Padic.exists_nat_eq_pow_mul (k : Nat.Primes → ℕ) (hk : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, k p = 0) : ∃ (D : ℕ) (D' : Nat.Primes → ℕ), D ≠ 0 ∧ (∀ (p : Nat.Primes), D = ↑p ^ k p * D' p) ∧ (∀ {p q : Nat.Primes}, q ≠ p → ↑q ^ k q ∣ D' p) ∧ ∀ (p : Nat.Primes), IsUnit ↑(D' p)

The integer D = ∏_p p ^ k p of a finitely supported family of exponents factors at each prime p as p ^ k p * D' p, where D' p is a p-adic unit divisible by q ^ k q for q ≠ p.