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 gauss_lemma_aux and
eisenstein_lemma_aux; they are used in quadratic_reciprocity.lean
to prove gauss_lemma and eisenstein_lemma, respectively.
@[simp]
theorem
legendre_symbol.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
theorem
legendre_symbol.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
theorem
legendre_symbol.sum_mul_div_add_sum_mul_div_eq_mul
(p q : ℕ)
[hp : fact (nat.prime p)]
(hq0 : ↑q ≠ 0) :
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.