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
{p : ℕ}
[h : Fact (Nat.Prime p)]
{a : ℤ}
(hp : p ≠ 2)
(ha0 : ↑a ≠ 0)
:
legendreSym p a = (-1) ^ Finset.card (Finset.filter (fun x => p / 2 < ZMod.val (↑a * ↑x)) (Finset.Ico 1 (Nat.succ (p / 2))))
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.card (Finset.filter (fun x => p / 2 < ZMod.val (↑a * ↑x)) (Finset.Ico 1 (Nat.succ (p / 2)))) ≡ 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.card (Finset.filter (fun x => x * b ≤ a) (Finset.Ico 1 (Nat.succ c)))
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