mathlib3

e6d01b8e - feat(topology/bounded_continuous_function): add `coe_mul`, `mul_apply` (#6867)

feat(topology/bounded_continuous_function): add `coe_mul`, `mul_apply` (#6867) Partners of the extant `coe_smul`, `smul_apply` lemmas (see line 630). These came up while working on the `replace_algebra_def` branch but seem worth adding independently.