mathlib3

01f1f1bc - feat(number_theory/legendre_symbol/add_character): change `coe_to_fun` for `add_char` so it includes `of_add` (#16016)

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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/map.20from.20mult.20gp.20to.20add.20gp/near/292623869) 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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60pnat.60.20vs.20.60.5Bfact.20.280.20.3C.20n.29.5D.60/near/293293368).