Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 21:53 abb635ff

View on Github →

feat(number_theory/legendre_symbol/quadratic_reciprocity): switch to Gauss sum proof, clean-up (#16171) This PR is (for now) the final step in the quest to change the proof of Quadratic Reciprocity from using the Gauss and Eisenstein lemmas to using the results for quadratic characters of general finite fields obtained from properties of the quadratic Gauss sum. In addition, there is some clean-up of the file and some further results (e.g., on the quadratic character of -2 and some versions of the law of quadratic reciprocity that are probably easier to use), and the documentation has been extended. The Gauss and Eisenstein lemmas have been moved to number_theory/legendre_symbol/gauss_eisenstein_lemmas (where the auxiliary results needed for them have already been residing). I have opened a topic on this under "PR reviews".

Estimated changes

added theorem quadratic_char_fun_mul
added theorem quadratic_char_fun_one
deleted theorem quadratic_char_mul
deleted theorem quadratic_char_one
modified theorem quadratic_char_zero
deleted theorem zmod.eisenstein_lemma
modified theorem zmod.euler_criterion
modified theorem zmod.euler_criterion_units
modified theorem zmod.exists_sq_eq_two_iff
deleted theorem zmod.gauss_lemma
modified def zmod.legendre_sym
modified theorem zmod.legendre_sym_eq_pow
modified def zmod.legendre_sym_hom
modified theorem zmod.legendre_sym_mod
modified theorem zmod.legendre_sym_mul
modified theorem zmod.legendre_sym_one
modified theorem zmod.legendre_sym_sq_one'
modified theorem zmod.legendre_sym_sq_one
modified theorem zmod.legendre_sym_two
modified theorem zmod.legendre_sym_zero
modified theorem zmod.quadratic_reciprocity