mathlib

440163b4 - chore(topology/algebra/mul_action): define `has_continuous_vadd` using `to_additive` (#10227)

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.