Commit 2021-06-21 03:37 4d69b0f4

chore(topology/algebra/infinite_sum): small todo (#7994) Generalize a lemma from f : ℕ → ℝ to f : β → α, with

[add_comm_group α] [topological_space α] [topological_add_group α] [t2_space α] [decidable_eq β] 

This was marked as TODO after #6017/#6096.