[Merged by Bors] - feat(Topology/Algebra): inv and div for infinite products over groups with zero

Mathlib/Topology/Algebra/InfiniteSum/Group.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 module
 
 public import Mathlib.SetTheory.Cardinal.Finite
+public import Mathlib.Topology.Algebra.GroupWithZero
 public import Mathlib.Topology.Algebra.InfiniteSum.Basic
 public import Mathlib.Topology.UniformSpace.Cauchy
 public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
@@ -460,4 +461,18 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
   obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
   exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable
 
+omit [SeparatelyContinuousMul K] in
+theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a) (ha : a ≠ 0) :
+    HasProd (fun x ↦ (f x )⁻¹) a⁻¹ := by
+  unfold HasProd
+  convert Filter.Tendsto.inv₀ h ha
+  rw [Finset.prod_inv_distrib]
+
+omit [SeparatelyContinuousMul K] in
+theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}
+    (hf : HasProd f a) (hg : HasProd g b) (hb : b ≠ 0) :
+    HasProd (fun x ↦ f x / g x) (a / b) := by
+  simp only [div_eq_mul_inv]
+  exact hf.mul <| hg.inv₀ hb
+
 end CommGroupWithZero