…coercions

There are a bunch of random specific versions of these lemmas floating around, which can be made generic to apply to all `one_hom_class`/`mul_hom_class`/`monoid_hom_class` instances. Compare existing `ring_hom.coe_coe`.

…quiv`

This PR adds more lemmas for the coercion of `refl` and `trans` of `{mul,add,ring}_equiv` to other types of maps. In particular, it ensures these types come with:
 * `coe_{type}_refl` and `coe_{type}_trans` where `type` ranges over the types of bundled maps that the equivs inherit from
 * `self_trans_symm` and `symm_trans_self`
 * `coe_trans`

Of course, it would be great if we figured out some generic way of stating all these results so we wouldn't have to go through and add all these lemmas.

…quiv`

This PR adds more lemmas for the coercion of `refl` and `trans` of `{mul,add,ring}_equiv` to other types of maps. In particular, it ensures these types come with:
 * `coe_{type}_refl` and `coe_{type}_trans` where `type` ranges over the types of bundled maps that the equivs inherit from
 * `self_trans_symm` and `symm_trans_self`
 * `coe_trans`

Of course, it would be great if we figured out some generic way of stating all these results so we wouldn't have to go through and add all these lemmas.

…to subgroup isomorphism

… fraction field

…-class-group