Commit 2022-07-23 21:26 983c737a

feat(number_theory/legendre_symbol/add_character): add file introducing additive characters (#15499) This adds a file that defines additive characters on commutative rings and proves some relevant properties, e.g., that on finite fields and rings of type zmod n, there exists a primitive additive character, and that the sum of the character values vanishes when the character is nontrivial. This will be used in a later PR (together with multiplicative characters) to define Gauss sums and prove some resuits on them. There is a Zulip topic to discuss this.