def PadicSameSquareClass (p : ℕ) [Fact (Nat.Prime p)] (a b : ℚ_[p]) : Prop

Two elements $a, b \in \mathbb{Q}_p$ lie in the same square class if there exists a nonzero $u \in \mathbb{Q}_p$ such that $a = b \cdot u^2$.

def RealSameSquareClass (a b : ℝ) : Prop

Two real numbers $a, b \in \mathbb{R}$ lie in the same square class if there exists a nonzero $u \in \mathbb{R}$ such that $a = b \cdot u^2$ (equivalently, $a$ and $b$ have the same sign).

theorem PadicSameSquareClass.refl {p : ℕ} [Fact (Nat.Prime p)] {a : ℚ_[p]} (_ha : a ≠ 0) : PadicSameSquareClass p a a

Reflexivity: any nonzero $a \in \mathbb{Q}_p$ is in the same square class as itself, witnessed by $u = 1$.

theorem PadicSameSquareClass.trans {p : ℕ} [Fact (Nat.Prime p)] {a b c : ℚ_[p]} (h1 : PadicSameSquareClass p a b) (h2 : PadicSameSquareClass p b c) : PadicSameSquareClass p a c

Transitivity of the same-square-class relation in $\mathbb{Q}_p$.

theorem square_class_mul_of_div {p : ℕ} [Fact (Nat.Prime p)] (r s : ℚ) (x : ℚ_[p]) (hx : x ≠ 0) (hs : s ≠ 0) (h : PadicSameSquareClass p (↑r) (↑s * x⁻¹)) : PadicSameSquareClass p (↑(r * s)) x

If $r$ is in the same square class as $s/x$ in $\mathbb{Q}_p$, then $r \cdot s$ is in the same square class as $x$. Used to rescale the approximating rational.

theorem real_same_sign_same_square_class (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hab : 0 < a * b) : RealSameSquareClass a b

Two nonzero real numbers with the same sign (equivalently, $a \cdot b > 0$) are in the same square class, witnessed by $u = \sqrt{a/b}$.

theorem padicValRat_prime_zpow (p : ℕ) [hp : Fact (Nat.Prime p)] (v : ℤ) : padicValRat p (↑p ^ v) = v

The $p$-adic valuation of $p^v$ in $\mathbb{Q}$ is $v$ (for $v \in \mathbb{Z}$).

theorem padicNorm_prime_self_zpow (p : ℕ) [hp : Fact (Nat.Prime p)] (v : ℤ) : padicNorm p (↑p ^ v) = ↑p ^ (-v)

The $p$-adic norm of $p^v$ in $\mathbb{Q}$ is $p^{-v}$.

theorem padicNorm_prime_zpow_ne (p q : ℕ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p ≠ q) (v : ℤ) : padicNorm q (↑p ^ v) = 1

For distinct primes $p \neq q$, the $q$-adic norm of $p^v$ is $1$ (since $p$ is a $q$-adic unit).

theorem padicNorm_prod_at_prime (n : ℕ) (primes : Fin n → ℕ) (hp : ∀ (i : Fin n), Fact (Nat.Prime (primes i))) (hinj : Function.Injective primes) (vals : Fin n → ℤ) (i : Fin n) : padicNorm (primes i) (∏ j : Fin n, ↑(primes j) ^ vals j) = padicNorm (primes i) (↑(primes i) ^ vals i)

Given pairwise distinct primes $p_0, \dots, p_{n-1}$, the $p_i$-adic norm of $\prod_j p_j^{v_j}$ equals the $p_i$-adic norm of $p_i^{v_i}$ alone (the other factors are units at $p_i$).

theorem padicNorm_prod_primes_eq_one (n : ℕ) (primes : Fin n → ℕ) (hp : ∀ (i : Fin n), Fact (Nat.Prime (primes i))) (vals : Fin n → ℤ) (q : ℕ) [hq : Fact (Nat.Prime q)] (hq_not : ∀ (i : Fin n), q ≠ primes i) : padicNorm q (∏ i : Fin n, ↑(primes i) ^ vals i) = 1

For a prime $q$ different from each $p_i$, the $q$-adic norm of $\prod_i p_i^{v_i}$ is $1$.

theorem padic_unit_square_class_of_congr (p : ℕ) [Fact (Nat.Prime p)] (u v : ℤ_[p]) (hu : IsUnit u) (hv : IsUnit v) (e : ℕ) (he : e = if p = 2 then 3 else 1) (hcong : (PadicInt.toZModPow e) u = (PadicInt.toZModPow e) v) : PadicSameSquareClass p ↑u ↑v

Two $p$-adic units $u, v \in \mathbb{Z}_p^\times$ that are congruent modulo $p^e$ (with $e = 3$ if $p = 2$ and $e = 1$ otherwise) are in the same square class in $\mathbb{Q}_p^\times$. The proof applies Hensel's lemma to the polynomial $X^2 - (u/v)$.

theorem exists_prime_approx_units (n : ℕ) (primes : Fin n → ℕ) (hp : ∀ (i : Fin n), Fact (Nat.Prime (primes i))) (hinj : Function.Injective primes) (u : (i : Fin n) → ℚ_[primes i]) (hu_unit : ∀ (i : Fin n), ‖u i‖ = 1) : ∃ (p₀ : ℕ), Nat.Prime p₀ ∧ (∀ (i : Fin n), p₀ ≠ primes i) ∧ ∀ (i : Fin n), PadicSameSquareClass (primes i) (↑↑p₀) (u i)

Existence of a simultaneous prime approximation. Given finitely many distinct primes $p_1, \dots, p_n$ and units $u_i \in \mathbb{Z}_{p_i}^\times$, there exists a prime $p_0$ not among the $p_i$ such that $p_0$ is in the same square class as $u_i$ in $\mathbb{Q}_{p_i}$ for each $i$. Combines CRT and Dirichlet's theorem on primes in arithmetic progressions.

theorem padic_unit_norm_of_prod_div (n : ℕ) (primes : Fin n → ℕ) (hp : ∀ (i : Fin n), Fact (Nat.Prime (primes i))) (_hinj : Function.Injective primes) (x_fin : (i : Fin n) → ℚ_[primes i]) (hx_fin : ∀ (i : Fin n), x_fin i ≠ 0) (y : ℚ) (_hy : y ≠ 0) (hy_norm : ∀ (i : Fin n), ‖↑y‖ = ‖x_fin i‖) (i : Fin n) : ‖↑y * (x_fin i)⁻¹‖ = 1

If a rational $y$ has the same $p_i$-adic norm as $x_i$ for each $i$, then $y \cdot x_i^{-1}$ is a unit in $\mathbb{Q}_{p_i}$ for each $i$.

theorem lemma_11_11 (n : ℕ) (primes : Fin n → ℕ) (hp : ∀ (i : Fin n), Fact (Nat.Prime (primes i))) (hinj : Function.Injective primes) (x_fin : (i : Fin n) → ℚ_[primes i]) (hx_fin : ∀ (i : Fin n), x_fin i ≠ 0) (infInS : Bool) (x_inf : ℝ) (hx_inf : infInS = true → x_inf ≠ 0) : ∃ (x : ℚ), x ≠ 0 ∧ (∀ (i : Fin n), PadicSameSquareClass (primes i) (↑x) (x_fin i)) ∧ (infInS = true → RealSameSquareClass (↑x) x_inf) ∧ ∃ (exceptions : Finset ℕ), exceptions.card ≤ 1 ∧ ∀ (q : ℕ) (_hq : Fact (Nat.Prime q)), q ∉ Finset.image primes Finset.univ → q ∉ exceptions → ‖↑x‖ = 1

Lemma 11.11 (Square-class weak approximation). Given a finite set $S$ of places of $\mathbb{Q}$ (a finite set of primes $\{p_i\}$, possibly together with the infinite place) and nonzero elements $x_i \in \mathbb{Q}_{p_i}^\times$ (and a sign $x_\infty \in \mathbb{R}^\times$ if the infinite place is in $S$), there exists $x \in \mathbb{Q}^\times$ that is in the same square class as $x_i$ at every place in $S$ and is a $q$-adic unit at every prime $q$ outside $S$, with at most one possible exception.