mathlib3

a32d58ba - feat(analysis/*): generalize `set_smul_mem_nhds_zero` to topological vector spaces (#12779)

feat(analysis/*): generalize `set_smul_mem_nhds_zero` to topological vector spaces (#12779) The lemma holds for arbitrary topological vector spaces and has nothing to do with normed spaces. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>