mathlib

474aecb9 - doc(algebra,data/fun_like): small morphism documentation improvements (#11642)

doc(algebra,data/fun_like): small morphism documentation improvements (#11642) * The `fun_like` docs talked about a `to_fun` class, this doesn't exist (anymore). * Warn that `{one,mul,monoid,monoid_with_zero}_hom.{congr_fun,congr_arg,coe_inj,ext_iff}` has been superseded by `fun_like`. Thanks to @YaelDillies for pointing out these issues.