mathlib3

54619e05 - feat(algebra/{hom,ring}): extra coercion lemmas for `{mul,add,ring}_equiv` (#16725)

feat(algebra/{hom,ring}): extra coercion lemmas for `{mul,add,ring}_equiv` (#16725) 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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>