Lemmas of Gauss and Eisenstein #

This file contains code for the proof of the Lemmas of Gauss and Eisenstein on the Legendre symbol. The main results are zmod.gauss_lemma_aux and zmod.eisenstein_lemma_aux.

source

@[simp]

theorem zmod.wilsons_lemma (p : ℕ) [fact (nat.prime p)] :

↑((p - 1).factorial) = -1

Wilson's Lemma: the product of 1, ..., p-1 is -1 modulo p.

source

@[simp]

theorem zmod.prod_Ico_one_prime (p : ℕ) [fact (nat.prime p)] :

(finset.Ico 1 p).prod (λ (x : ℕ), ↑x) = -1

source

theorem zmod.Ico_map_val_min_abs_nat_abs_eq_Ico_map_id (p : ℕ) [hp : fact (nat.prime p)] (a : zmod p) (hap : a ≠ 0) :

multiset.map (λ (x : ℕ), (a * ↑x).val_min_abs.nat_abs) (finset.Ico 1 (p / 2).succ).val = multiset.map (λ (a : ℕ), a) (finset.Ico 1 (p / 2).succ).val

The image of the map sending a non zero natural number x ≤ p / 2 to the absolute value of the element of interger in the interval (-p/2, p/2] congruent to a * x mod p is the set of non zero natural numbers x such that x ≤ p / 2

source

theorem zmod.gauss_lemma_aux (p : ℕ) [hp : fact (nat.prime p)] [fact (p % 2 = 1)] {a : ℤ} (hap : ↑a ≠ 0) :

↑a ^ (p / 2) = (-1) ^ (finset.filter (λ (x : ℕ), p / 2 < (↑a * ↑x).val) (finset.Ico 1 (p / 2).succ)).card

source

theorem zmod.gauss_lemma {p : ℕ} [fact (nat.prime p)] {a : ℤ} (hp : p ≠ 2) (ha0 : ↑a ≠ 0) :

legendre_sym p a = (-1) ^ (finset.filter (λ (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

source

theorem zmod.eisenstein_lemma_aux (p : ℕ) [fact (nat.prime p)] [fact (p % 2 = 1)] {a : ℕ} (ha2 : a % 2 = 1) (hap : ↑a ≠ 0) :

(finset.filter (λ (x : ℕ), p / 2 < (↑a * ↑x).val) (finset.Ico 1 (p / 2).succ)).card ≡ (finset.Ico 1 (p / 2).succ).sum (λ (x : ℕ), x * a / p) [MOD 2]

source

theorem zmod.div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) :

a / b = (finset.filter (λ (x : ℕ), x * b ≤ a) (finset.Ico 1 c.succ)).card

source

theorem zmod.sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : fact (nat.prime p)] (hq0 : ↑q ≠ 0) :

(finset.Ico 1 (p / 2).succ).sum (λ (a : ℕ), a * q / p) + (finset.Ico 1 (q / 2).succ).sum (λ (a : ℕ), a * p / q) = p / 2 * (q / 2)

Each of the sums in this lemma is the cardinality of the set 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.

source

theorem zmod.eisenstein_lemma {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : ↑a ≠ 0) :

legendre_sym p ↑a = (-1) ^ (finset.Ico 1 (p / 2).succ).sum (λ (x : ℕ), x * a / p)