# Commit 2022-08-16 16:11 01f1f1bc

View on Github →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.