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.

Estimated changes

Modified src/topology/continuous_function/algebra.lean

deleted def coe_fn_monoid_hom

added def continuous_map.coe_fn_monoid_hom

modified theorem continuous_map.coe_prod

added def continuous_map.comp_monoid_hom'

modified theorem continuous_map.div_coe

modified theorem continuous_map.div_comp

modified theorem continuous_map.inv_coe

modified theorem continuous_map.inv_comp

added theorem continuous_map.one_comp

modified theorem continuous_map.pow_coe

modified theorem continuous_map.pow_comp

modified theorem continuous_map.prod_apply

modified theorem continuous_map.smul_apply

modified theorem continuous_map.smul_coe

modified theorem continuous_map.smul_comp