mathlib

92b90480 - chore(topology/continuous_function/algebra): put `coe_fn_monoid_hom `into the `continuous_map` namespace (#7423)

chore(topology/continuous_function/algebra): put `coe_fn_monoid_hom `into the `continuous_map` namespace (#7423) Rather than adding `continuous_map.` to the definition, this wraps everything in a namespace to make this type of mistake unlikely to happen again. This also adds `comp_monoid_hom'` to golf a proof.