Commit 2023-06-26 13:08 dc08a85f

View on Github →

feat: port NumberTheory.LegendreSymbol.QuadraticReciprocity (#5483)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean

added theorem ZMod.exists_sq_eq_neg_two_iff

added theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one

added theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three

added theorem ZMod.exists_sq_eq_two_iff

added theorem legendreSym.at_neg_two

added theorem legendreSym.at_two

added theorem legendreSym.quadratic_reciprocity'

added theorem legendreSym.quadratic_reciprocity

added theorem legendreSym.quadratic_reciprocity_one_mod_four

added theorem legendreSym.quadratic_reciprocity_three_mod_four