Quadratic reciprocity.
This file contains results about quadratic residues modulo a prime number.
The main results are the law of quadratic reciprocity, quadratic_reciprocity, as well as the
interpretations in terms of existence of square roots depending on the congruence mod 4,
exists_pow_two_eq_prime_iff_of_mod_four_eq_one, and
exists_pow_two_eq_prime_iff_of_mod_four_eq_three.
Also proven are conditions for -1 and 2 to be a square modulo a prime,
exists_pow_two_eq_neg_one_iff_mod_four_ne_three and
exists_pow_two_eq_two_iff
Implementation notes
The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein's lemma
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
The Legendre symbol of a and p is an integer defined as
0ifais0modulop;1ifa ^ (p / 2)is1modulop(byeuler_criterionthis is equivalent to “ais a square modulop”);-1otherwise.