mathlib3

2a2d33c8 - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean (#15684)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gauss.20sums/near/290844370).