theorem hilbert_symm {F : Type u_1} [Field F] (a b : Fˣ) : hilbertSymbol F a b = hilbertSymbol F b a

Symmetry of the Hilbert symbol: $(a, b)_F = (b, a)_F$, since the equation $ax^2 + by^2 = 1$ is equivalent to $by^2 + ax^2 = 1$.

theorem hilbert_mul_right_of_eq_one {F : Type u_1} [Field F] [CharZero F] (a b c : Fˣ) (h : hilbertSymbol F a b = 1) : hilbertSymbol F a (b * c) = hilbertSymbol F a c

Bilinearity in the second argument when $(a, b)_F = 1$: in that case, $(a, bc)_F = (a, c)_F$. Follows from symmetry and hilbert_mul_of_eq_one.

noncomputable def qpPrime (p : ℕ) [Fact (Nat.Prime p)] : ℚ_[p]ˣ

The prime $p$ viewed as a unit in $\mathbb{Q}_p^\times$.

noncomputable def padicUnitLegendre {p : ℕ} [hp : Fact (Nat.Prime p)] (v : ℤ_[p]ˣ) : ℤ

The Legendre symbol $\left(\frac{v}{p}\right)$ of a $p$-adic unit $v \in \mathbb{Z}_p^\times$, computed via the reduction mod $p$.

noncomputable def padicPowerUnit (p : ℕ) [Fact (Nat.Prime p)] (α : Fin 2) (u : ℤ_[p]ˣ) : ℚ_[p]ˣ

A "primitive-unit" representative $p^\alpha \cdot u \in \mathbb{Q}_p^\times$ with exponent $\alpha \in \{0, 1\}$ and $u$ a $p$-adic integer unit.

theorem toZMod_p_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : PadicInt.toZMod ↑p = 0

The image of $p$ under the reduction map $\mathbb{Z}_p \to \mathbb{Z}/p$ is zero.

theorem norm_lt_one_iff_toZMod_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ‖x‖ < 1 ↔ PadicInt.toZMod x = 0

For $x \in \mathbb{Z}_p$: $\|x\| < 1$ iff $x \equiv 0 \pmod{p}$.

theorem isUnit_iff_toZMod_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : IsUnit x ↔ PadicInt.toZMod x ≠ 0

For $x \in \mathbb{Z}_p$: $x$ is a unit iff its reduction mod $p$ is non-zero.

theorem dvd_iff_toZMod_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ↑p ∣ x ↔ PadicInt.toZMod x = 0

For $x \in \mathbb{Z}_p$: $p \mid x$ iff $x \equiv 0 \pmod p$.

theorem legendreSym_val_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (v : ℤ_[p]ˣ) : ↑(PadicInt.toZMod ↑v).val = PadicInt.toZMod ↑v

The natural number value of $\bar v \in \mathbb{Z}/p$, viewed back in $\mathbb{Z}/p$, recovers $\bar v$ itself. Used to compute the Legendre symbol.

theorem padicUnitLegendre_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (v : ℤ_[p]ˣ) : ↑(PadicInt.toZMod ↑v).val ≠ 0

The integer representative of $v \bmod p$ is non-zero in $\mathbb{Z}/p$ (since $v$ is a unit, its reduction is non-zero).

theorem hilbert_p_unit_eq_legendre {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (v : ℤ_[p]ˣ) : padicHilbertSymbol p (qpPrime p) (HilbertSymbol.unitZpToQp v) = padicUnitLegendre v

(Textbook Lemma 10.8) For an odd prime $p$ and $v \in \mathbb{Z}_p^\times$, the Hilbert symbol $(p, v)_p$ equals the Legendre symbol $\left(\frac{v}{p}\right)$.

theorem hilbert_formula_odd {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (α β : Fin 2) (u v : ℤ_[p]ˣ) : padicHilbertSymbol p (padicPowerUnit p α u) (padicPowerUnit p β v) = (-1) ^ (↑α * ↑β * ((p - 1) / 2)) * padicUnitLegendre u ^ ↑β * padicUnitLegendre v ^ ↑α

(Textbook Theorem 10.7, exponents in $\{0, 1\}$) For an odd prime $p$, exponents $\alpha, \beta \in \{0, 1\}$, and units $u, v \in \mathbb{Z}_p^\times$, the Hilbert symbol of $p^\alpha u$ and $p^\beta v$ is given by $$(p^\alpha u, p^\beta v)_p = (-1)^{\alpha\beta \cdot \frac{p-1}{2}} \left(\tfrac{u}{p}\right)^\beta \left(\tfrac{v}{p}\right)^\alpha.$$

noncomputable def padicPowerUnitZ (p : ℕ) [Fact (Nat.Prime p)] (α : ℤ) (u : ℤ_[p]ˣ) : ℚ_[p]ˣ

A "primitive-unit" representative $p^\alpha \cdot u \in \mathbb{Q}_p^\times$ with integer exponent $\alpha \in \mathbb{Z}$ (allowing both positive and negative powers of $p$).

theorem hilbert_sq_left {p : ℕ} [hp : Fact (Nat.Prime p)] (s b : ℚ_[p]ˣ) : hilbertSymbol ℚ_[p] (s ^ 2) b = 1

The Hilbert symbol is trivial on squares: $(s^2, b)_p = 1$ for any $s, b$.

theorem hilbert_sq_mul_left {p : ℕ} [hp : Fact (Nat.Prime p)] (s a b : ℚ_[p]ˣ) : hilbertSymbol ℚ_[p] (s ^ 2 * a) b = hilbertSymbol ℚ_[p] a b

Square-invariance of the Hilbert symbol in the first argument: $(s^2 \cdot a, b)_p = (a, b)_p$.

theorem hilbert_sq_mul_right {p : ℕ} [hp : Fact (Nat.Prime p)] (s a b : ℚ_[p]ˣ) : hilbertSymbol ℚ_[p] a (s ^ 2 * b) = hilbertSymbol ℚ_[p] a b

Square-invariance of the Hilbert symbol in the second argument: $(a, s^2 \cdot b)_p = (a, b)_p$.

theorem int_emod_two_toNat_lt (α : ℤ) : (α % 2).toNat < 2

The natural number $(α \bmod 2).\text{toNat}$ is strictly less than $2$.

theorem hilbert_padicPowerUnitZ_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (α : ℤ) (u : ℤ_[p]ˣ) (b : ℚ_[p]ˣ) : hilbertSymbol ℚ_[p] (padicPowerUnitZ p α u) b = hilbertSymbol ℚ_[p] (padicPowerUnit p ⟨(α % 2).toNat, ⋯⟩ u) b

Reduces a padicPowerUnitZ (integer exponent) to a padicPowerUnit ($\{0, 1\}$ exponent) inside the Hilbert symbol, using square-invariance: $p^{2k} \cdot$(anything) leaves the Hilbert symbol unchanged.

theorem pow_eq_of_sq_eq_one_of_mod_two_eq {x : ℤ} (hx : x ^ 2 = 1) {a b : ℕ} (h : a % 2 = b % 2) : x ^ a = x ^ b

If $x^2 = 1$ (i.e., $x = \pm 1$), then $x^a = x^b$ whenever $a \equiv b \pmod 2$.

theorem int_emod_two_toNat_mod_two_eq_natAbs_mod_two (α : ℤ) : (α % 2).toNat % 2 = α.natAbs % 2

The natural number $(α \bmod 2).\text{toNat}$ has the same parity as $|α|$.

theorem padicUnitLegendre_sq {p : ℕ} [hp : Fact (Nat.Prime p)] (v : ℤ_[p]ˣ) : padicUnitLegendre v ^ 2 = 1

The Legendre symbol squared equals $1$, since it takes values in $\{\pm 1\}$.

theorem hilbert_formula_odd_general {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (α β : ℤ) (u v : ℤ_[p]ˣ) : padicHilbertSymbol p (padicPowerUnitZ p α u) (padicPowerUnitZ p β v) = (-1) ^ (α.natAbs * β.natAbs * ((p - 1) / 2)) * padicUnitLegendre u ^ β.natAbs * padicUnitLegendre v ^ α.natAbs

(Textbook Theorem 10.7, general form with integer exponents) For an odd prime $p$, integer exponents $\alpha, \beta \in \mathbb{Z}$, and units $u, v \in \mathbb{Z}_p^\times$, the Hilbert symbol of $p^\alpha u$ and $p^\beta v$ is $$(p^\alpha u, p^\beta v)_p = (-1)^{|\alpha|\,|\beta|\,\frac{p-1}{2}} \left(\tfrac{u}{p}\right)^{|\beta|} \left(\tfrac{v}{p}\right)^{|\alpha|}.$$