∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (a : α)
  (L : SummationFilter β), HasProd f a L = Filter.Tendsto (fun s => ∏ b ∈ s, f b) L.filter (nhds a)