Commit 2021-05-01 15:16 92b90480
View on Github →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.