Commit 2022-08-16 16:11 01f1f1bc

feat(number_theory/legendre_symbol/add_character): change coe_to_fun for add_char so it includes of_add (#16016) 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.