Commit 2022-02-16 14:23 e8156757

chore(topology/algebra/module/basic): remove two duplicate lemmas (#12072) continuous_linear_map.continuous_nsmul is nothing to do with continuous_linear_maps, 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.