∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α} {a₁ a₂ : α},
  HasProd f a₁ L → HasProd g a₂ L → HasProd (fun b => f b / g b) (a₁ / a₂) L