Commit 2021-04-06 05:50 975f5333

View on Github →

chore(topology/continuous_function/algebra): add simp lemmas for smul coercion, move names out of global namespace (#7007) The two new lemmas proposed are:

continuous_map.smul_coe
continuous_functions.smul_coe

Estimated changes

Modified src/topology/continuous_function/algebra.lean

added theorem continuous_functions.smul_coe

added theorem continuous_map.div_coe

added theorem continuous_map.inv_coe

added theorem continuous_map.pow_coe

modified theorem continuous_map.smul_apply

added theorem continuous_map.smul_coe

deleted theorem div_coe

deleted theorem inv_coe

deleted theorem pow_coe