Commit 2021-03-25 21:40 e6d01b8e

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.