# 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 p.Prime] (a : ZMod p) (hap : a 0) :
Multiset.map (fun (x : ) => (a * x).valMinAbs.natAbs) (Finset.Ico 1 (p / 2).succ).val = Multiset.map (fun (a : ) => a) (Finset.Ico 1 (p / 2).succ).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 p.Prime] {a : } (hap : a 0) :
a ^ (p / 2) = ((-1) ^ (Finset.filter (fun (x : ) => p / 2 < (a * x).val) (Finset.Ico 1 (p / 2).succ)).card)
theorem ZMod.gauss_lemma {p : } [h : Fact p.Prime] {a : } (hp : p 2) (ha0 : a 0) :
= (-1) ^ (Finset.filter (fun (x : ) => p / 2 < (a * x).val) (Finset.Ico 1 (p / 2).succ)).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 p.Prime] [Fact (p % 2 = 1)] {a : } (ha2 : a % 2 = 1) (hap : a 0) :
(Finset.filter (fun (x : ) => p / 2 < (a * x).val) (Finset.Ico 1 (p / 2).succ)).card xFinset.Ico 1 (p / 2).succ, 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 c.succ)).card
theorem ZMod.sum_mul_div_add_sum_mul_div_eq_mul (p : ) (q : ) [hp : Fact p.Prime] (hq0 : q 0) :
aFinset.Ico 1 (p / 2).succ, a * q / p + aFinset.Ico 1 (q / 2).succ, 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 p.Prime] (hp : p 2) {a : } (ha1 : a % 2 = 1) (ha0 : a 0) :
legendreSym p a = (-1) ^ xFinset.Ico 1 (p / 2).succ, x * a / p

Eisenstein's lemma