mathlib

mathlib copied to clipboard

The purpose of this PR is to carry out the solution mentioned here to the unpleasantness that one has to explicitly invoke of_add and to_add when working with homomorphisms from additive to multiplicative monoids (in the form multiplicative M → M'). The idea is to implement the coercion to a function M → M' so that it inserts the to_add conversion automatically.

This is done here for additive characters (which also simplifies the treatment of Gauss sums in number_theory/legendre_symbol/gauss_sum).

We also change many nat arguments in add_character.lean to pnat, to help the with the refactor of cyclotomic fields. See the discussion here.

---