Commit 2022-08-16 16:11 01f1f1bcView on Github →
add_char so it includes
The purpose of this PR is to carry out the solution mentioned here to the unpleasantness that one has to explicitly invoke
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
We also change many
nat arguments in
pnat, to help the with the refactor of cyclotomic fields. See the discussion here.