Lemmas of Gauss and Eisenstein

This file contains the Lemmas of Gauss and Eisenstein on the Legendre symbol. The main results are ZMod.gauss_lemma and ZMod.eisenstein_lemma.

theorem ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ZMod p) (hap : a ≠ 0) : Multiset.map (fun (x : ℕ) => Int.natAbs (ZMod.valMinAbs (a * ↑x))) (Finset.Ico 1 (Nat.succ (p / 2))).val = Multiset.map (fun (a : ℕ) => a) (Finset.Ico 1 (Nat.succ (p / 2))).val

The image of the map sending a nonzero natural number x ≤ p / 2 to the absolute value of the integer in (-p/2, p/2] that is congruent to a * x mod p is the set of nonzero natural numbers x such that x ≤ p / 2.

theorem ZMod.gauss_lemma_aux (p : ℕ) [hp : Fact (Nat.Prime p)] {a : ℤ} (hap : ↑a ≠ 0) : ↑a ^ (p / 2) = ↑((-1) ^ (Finset.filter (fun (x : ℕ) => p / 2 < ZMod.val (↑a * ↑x)) (Finset.Ico 1 (Nat.succ (p / 2)))).card)

theorem ZMod.gauss_lemma {p : ℕ} [h : Fact (Nat.Prime p)] {a : ℤ} (hp : p ≠ 2) (ha0 : ↑a ≠ 0) : legendreSym p a = (-1) ^ (Finset.filter (fun (x : ℕ) => p / 2 < ZMod.val (↑a * ↑x)) (Finset.Ico 1 (Nat.succ (p / 2)))).card

Gauss' lemma. The Legendre symbol can be computed by considering the number of naturals less than p/2 such that (a * x) % p > p / 2.

theorem ZMod.eisenstein_lemma_aux (p : ℕ) [Fact (Nat.Prime p)] [Fact (p % 2 = 1)] {a : ℕ} (ha2 : a % 2 = 1) (hap : ↑a ≠ 0) : (Finset.filter (fun (x : ℕ) => p / 2 < ZMod.val (↑a * ↑x)) (Finset.Ico 1 (Nat.succ (p / 2)))).card ≡ Finset.sum (Finset.Ico 1 (Nat.succ (p / 2))) fun (x : ℕ) => x * a / p [MOD 2]

theorem ZMod.div_eq_filter_card {a : ℕ} {b : ℕ} {c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) : a / b = (Finset.filter (fun (x : ℕ) => x * b ≤ a) (Finset.Ico 1 (Nat.succ c))).card

theorem ZMod.sum_mul_div_add_sum_mul_div_eq_mul (p : ℕ) (q : ℕ) [hp : Fact (Nat.Prime p)] (hq0 : ↑q ≠ 0) : ((Finset.sum (Finset.Ico 1 (Nat.succ (p / 2))) fun (a : ℕ) => a * q / p) + Finset.sum (Finset.Ico 1 (Nat.succ (q / 2))) fun (a : ℕ) => a * p / q) = p / 2 * (q / 2)

Each of the sums in this lemma is the cardinality of the set of integer points in each of the two triangles formed by the diagonal of the rectangle (0, p/2) × (0, q/2). Adding them gives the number of points in the rectangle.

theorem ZMod.eisenstein_lemma {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : ↑a ≠ 0) : legendreSym p ↑a = (-1) ^ Finset.sum (Finset.Ico 1 (Nat.succ (p / 2))) fun (x : ℕ) => x * a / p

Eisenstein's lemma