chore(algebra/ring/basic): docs, simps (#4375)
* add docstrings to all typeclasses in `algebra/ring/basic`;
* add `ring_hom.inhabited := ⟨id α⟩` to make linter happy;
* given `f : α →+* β`, simplify `f.to_monoid_hom` and
`f.to_add_monoid_hom` to coercions;
* add `simp` lemmas for coercions of `ring_hom.mk f _ _ _ _` to
`monoid_hom` and `add_monoid_hom`.
