mathlib3

e8156757 - chore(topology/algebra/module/basic): remove two duplicate lemmas (#12072)

chore(topology/algebra/module/basic): remove two duplicate lemmas (#12072) `continuous_linear_map.continuous_nsmul` is nothing to do with `continuous_linear_map`s, and is the same as `continuous_nsmul`, but the latter doesn't require commutativity. There is no reason to keep the former. This lemma was added in #7084, but probably got missed due to how large that PR had to be. We can't remove `continuous_linear_map.continuous_zsmul` until #12055 is merged, as there is currently no `continuous_zsmul` in the root namespace.