[Merged by Bors] - feat(number_theory/legendre_symbol/add_character): add file introducing additive characters

[MichaelStollBayreuth]

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.

---

[kbuzzard]

I've only looked through about the first half, and golfed a couple of proofs; certainly this material should be in mathlib though.

[kbuzzard]

For me this PR raises an interesting question. My impression is that the community are not keen on adding the structure of maps f:A -> G such that f(a+b)=f(a)*f(b), because then we have to make an API for it, and how it composes with additive maps on one side and multiplicative maps on the other side, and then there are maps G -> A and etc etc. Another proposal is to define add_char so that it contains an application of of_add : R -> multiplicative R and then just write add_char.map_add : \psi (a + b) = \psi a * \psi b and a bit more API for it.

My position on this has come from a huge struggle I had in the past using with_top because it would often leak to option, and if you were working with with_top and with_bot then you didn't know whether none was bot or top. Being principled with types in statements of results goes a long way towards stopping this kind of leakage.

[MichaelStollBayreuth]

To add to @kbuzzard 's comment above, I find it quite painful to have to use multiplicative R →* R' instead of something like, say, R +→* R' and having to convert between R and multiplicative R via of_add and to_add. (And as one can see from Kevin's comments, I didn't manage to do it completely right...). If homomorphisms between additive and multiplicative structures also occur in some other places, it may be worth the effort of having dedicated type classes and API for them. Maybe there is a way of auto-generate them, something like a "left" or "right" version of to_additive?

[kbuzzard]

This is looking great. I've now read all of the PR and have suggested the way to go if you want to avoid defeq abuse.

[jcommelin]

Please fix the spacing. After that, you can send the PR to the queue with bors merge.

bors d+

[bors]

✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[MichaelStollBayreuth]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests