Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-09 19:12 4a1b5307

View on Github →

feat(number_theory/legendre_symbol/quadratic_char): add results on special values (#15888) This uses the new results on Gauss sums to prove results on the values of quadratic characters at 2, -2 and odd primes. The next step will be to use these to prove Quadratic Reciprocity and the Second Supplementary Law for Legendre symbols. Here is the Zulip discussion on Gauss sums.

Estimated changes

modified theorem finite_field.two_pow_card
added theorem mul_char.map_ring_char
deleted def char.quadratic_char
deleted theorem char.quadratic_char_mul
deleted theorem char.quadratic_char_one
deleted theorem char.quadratic_char_zero
added def quadratic_char
added theorem quadratic_char_mul
added theorem quadratic_char_neg_one
added theorem quadratic_char_neg_two
added theorem quadratic_char_one
added theorem quadratic_char_sq_one'
added theorem quadratic_char_sq_one
added theorem quadratic_char_two
added theorem quadratic_char_zero