chore(*): add docs and nolints (#2990)
Other changes:
* Reuse `gmultiples_hom` for `AddCommGroup.as_hom`.
* Reuse `add_monoid_hom.ext_int` for `AddCommGroup.int_hom_ext`.
* Drop the following definitions, define an `instance` right away
instead:
- `algebra.div`;
- `monoid_hom.one`, `add_monoid_hom.zero`;
- `monoid_hom.mul`, `add_monoid_hom.add`;
- `monoid_hom.inv`, `add_monoid_hom.neg`.
