hom): use `coe_comp` in `simp` lemmas (#4780)

Commit

5 years ago

chore(algebra/group/hom): use `coe_comp` in `simp` lemmas (#4780) This way Lean will simplify `⇑(f.comp g)` even if it is not applied to an element.

References

Author

urkud

Parents