Commit 2022-08-02 15:18 2a2d33c8

feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean (#15684) This adds a file to the number_theory/legendre_symbol directory. It defines the Gauss sum of a multiplicative and an additive character on a finite commutative ring with values in another commutative ring and proves some statements about them. This will lead to a new proof of Quadratic Reciprocity (including the second supplementary law). For comments/discussion, use this Zulip topic.