chore(algebra/char_zero): rename vars, add `with_top` instance (#4523)
Motivated by #3135.
* Use `R` as a `Type*` variable;
* Add `add_monoid_hom.map_nat_cast` and `with_top.coe_add_hom`;
* Drop versions of `char_zero_of_inj_zero`, use `[add_left_cancel_monoid R]` instead.