Commit 2021-11-08 22:17 440163b4

chore(topology/algebra/mul_action): define has_continuous_vadd using to_additive (#10227) Make additive version of the theory of has_continuous_smul, i.e., has_continuous_vadd, using to_additive. I've been fairly conservative in adding to_additive tags -- I left them off lemmas that didn't seem like they'd be relevant for typical additive actions, like those about units or group_with_zero. Also make normed_add_torsor an instance of has_continuous_vadd and use this to establish some of its continuity API.