hom): Add `mk_coe` lemmas (#5812)

Commit

5 years ago

chore(algebra/group/hom): Add `mk_coe` lemmas (#5812) These are the counterparts to the `coe_mk` lemmas.

Author

eric-wieser

Parents