algebra): add simp lemmas for smul coercion, move names out of global namespace (#7007)

Commit

5 years ago

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`

Author

ocfnash

Parents

90e265ea

mathlib 975f5333 - chore(topology/continuous_function/algebra): add simp lemmas for smul coercion, move names out of global namespace (#7007)

mathlib
975f5333 - chore(topology/continuous_function/algebra): add simp lemmas for smul coercion, move names out of global namespace (#7007)