Commit 2022-10-06 07:37 54619e05

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.