theorem PadicInt.toZModPow_surjective' {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : Function.Surjective ⇑(toZModPow n)

The reduction map $\mathbb{Z}_p \to \mathbb{Z}/p^n\mathbb{Z}$ is surjective.

theorem PadicInt.toZModPow_eq_zero_iff_dvd {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : (toZModPow n) x = 0 ↔ ↑p ^ n ∣ x

An element of $\mathbb{Z}_p$ reduces to zero mod $p^n$ iff it is divisible by $p^n$.

theorem PadicInt.isUnit_toZModPow_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) {x : ℤ_[p]} : IsUnit ((toZModPow n) x) ↔ IsUnit x

For $n \geq 1$, an element of $\mathbb{Z}_p$ is a unit iff its reduction mod $p^n$ is a unit.

def HasPrimitiveSolutionMod8_one (u v : ℤ_[2]ˣ) : Prop

Primitive mod-$8$ solvability of $z^2 = u x^2 + v y^2$ over $\mathbb{Z}_2$: there exist $x_0, y_0, z_0 \in \mathbb{Z}/8\mathbb{Z}$, not all non-units, satisfying the equation.

def HasPrimitiveSolutionMod8_two (u v : ℤ_[2]ˣ) : Prop

Primitive mod-$8$ solvability of $z^2 = 2u x^2 + v y^2$ over $\mathbb{Z}_2$.

noncomputable def padicUnit_one (u : ℤ_[2]ˣ) : ℚ_[2]ˣ

Lift of a $\mathbb{Z}_2$-unit to a $\mathbb{Q}_2$-unit (i.e. multiplication by $1$).

noncomputable def padicUnit_two (u : ℤ_[2]ˣ) : ℚ_[2]ˣ

The $\mathbb{Q}_2$-unit $2u$ obtained by multiplying the lift of u by $2$.

theorem norm_two_padic : ‖2‖ = 2⁻¹

The $2$-adic norm of $2$ equals $1/2$.

theorem exists_mul_sq_eq_of_mod8 {a c z : ℤ_[2]} (ha : IsUnit a) (hz : IsUnit z) (hdvd : 2 ^ 3 ∣ a * z ^ 2 - c) : ∃ (z' : ℤ_[2]), a * z' ^ 2 = c ∧ IsUnit z'

Hensel-lifting consequence: if $a$ is a unit, $z$ is a unit, and $az^2 \equiv c \pmod 8$, then there exists a unit $z'$ with $a (z')^2 = c$ exactly.

theorem padicUnit_one_val (u : ℤ_[2]ˣ) : ↑(padicUnit_one u) = ↑↑u

The underlying $\mathbb{Q}_2$-value of padicUnit_one u is the image of u.

theorem padicUnit_two_val (u : ℤ_[2]ˣ) : ↑(padicUnit_two u) = 2 * ↑↑u

The underlying $\mathbb{Q}_2$-value of padicUnit_two u is $2u$.

theorem lift_eq_to_Qp {a b : ℤ_[2]} (h : a = b) : ↑a = ↑b

Equal elements of $\mathbb{Z}_2$ map to equal elements of $\mathbb{Q}_2$.

theorem lemma_10_8_one (u v : ℤ_[2]ˣ) : HilbertSymbol.HasPrimitiveSolution (padicUnit_one u) (padicUnit_one v) ↔ HasPrimitiveSolutionMod8_one u v

Lemma 10.8 (case $\alpha = 0$): the equation $z^2 = u x^2 + v y^2$ has a primitive solution over $\mathbb{Q}_2$ iff it has a primitive solution mod $8$.

theorem no_prim_sol_two_x_unit (u₀ v₀ : (ZMod (2 ^ 3))ˣ) (x₀ y₀ z₀ : ZMod (2 ^ 3)) : IsUnit x₀ → ¬IsUnit y₀ → ¬IsUnit z₀ → z₀ ^ 2 = 2 * ↑u₀ * x₀ ^ 2 + ↑v₀ * y₀ ^ 2 → False

Brute-force verification: if $x_0$ is a unit and neither $y_0$ nor $z_0$ is a unit, then $z_0^2 = 2 u_0 x_0^2 + v_0 y_0^2$ has no solution mod $8$.

theorem lemma_10_8_two (u v : ℤ_[2]ˣ) : HilbertSymbol.HasPrimitiveSolution (padicUnit_two u) (padicUnit_one v) ↔ HasPrimitiveSolutionMod8_two u v

Lemma 10.8 (case $\alpha = 1$): the equation $z^2 = 2u x^2 + v y^2$ has a primitive solution over $\mathbb{Q}_2$ iff it has a primitive solution mod $8$.