noncomputable def diagQuadMvPoly {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (a : Fin n → ZMod p) : MvPolynomial (Fin n) (ZMod p)

The diagonal quadratic multivariate polynomial $\sum_i a_i X_i^2$ over $\mathbb{Z}/p$.

theorem exists_nontrivial_zero_mod_p {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 2 < n) (a : Fin n → ZMod p) : ∃ (y : Fin n → ZMod p), (∃ (i : Fin n), y i ≠ 0) ∧ ∑ i : Fin n, a i * y i ^ 2 = 0

Chevalley-Warning consequence. For $n > 2$, any diagonal quadratic form $\sum_i a_i y_i^2$ over $\mathbb{Z}/p$ has a nontrivial zero.

theorem norm_natCast_eq_one_of_not_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : ¬p ∣ n) : ‖↑n‖ = 1

If a natural number $n$ is not divisible by $p$, then the $p$-adic norm of $n$ is $1$.

theorem norm_mul_padic {p : ℕ} [hp : Fact (Nat.Prime p)] (a b : ℤ_[p]) : ‖a * b‖ = ‖a‖ * ‖b‖

Multiplicativity of the $p$-adic norm on $\mathbb{Z}_p$.

theorem norm_unit_eq_one {p : ℕ} [hp : Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : ‖↑u‖ = 1

Any unit $u \in \mathbb{Z}_p^\times$ has norm $1$.

noncomputable def quadPoly {p : ℕ} [hp : Fact (Nat.Prime p)] (a c : ℤ_[p]) : Polynomial ℤ_[p]

The univariate quadratic polynomial $c + a X^2 \in \mathbb{Z}_p[X]$.

theorem quadPoly_aeval {p : ℕ} [hp : Fact (Nat.Prime p)] (a c t : ℤ_[p]) : (Polynomial.aeval t) (quadPoly a c) = c + a * t ^ 2

Evaluation of quadPoly a c at $t$ equals $c + a t^2$.

theorem quadPoly_derivative_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (a c : ℤ_[p]) : Polynomial.derivative (quadPoly a c) = Polynomial.C (2 * a) * Polynomial.X

The derivative of quadPoly a c equals $2 a X$.

theorem quadPoly_aeval_derivative {p : ℕ} [hp : Fact (Nat.Prime p)] (a c t : ℤ_[p]) : (Polynomial.aeval t) (Polynomial.derivative (quadPoly a c)) = 2 * a * t

Evaluation of the derivative of quadPoly a c at $t$ equals $2 a t$.

theorem diagonal_unit_form_represents_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (hodd : p ≠ 2) {n : ℕ} (hn : 2 < n) (a : Fin n → ℤ_[p]ˣ) : ∃ (x : Fin n → ℚ_[p]), (∃ (i : Fin n), x i ≠ 0) ∧ ∑ i : Fin n, ↑↑(a i) * x i ^ 2 = 0

Theorem 11.1. Over $\mathbb{Q}_p$ with $p$ odd, any diagonal quadratic form $\sum_{i=1}^n a_i x_i^2$ in more than $2$ variables with unit coefficients $a_i \in \mathbb{Z}_p^\times$ has a nontrivial zero. The proof combines Chevalley-Warning (for a nontrivial zero mod $p$) with Hensel's lemma (to lift to $\mathbb{Z}_p$).