From cba9e1e72d2f22ba6e8b050bdf3778ec402db5bd Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Sun, 14 Jun 2026 09:10:27 +0100
Subject: [PATCH 1/9] feat(Topology.Algebra): inv and div for infinite products
 over groups with zero

---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 59d7d6eb32c464..15e464eae4914c 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/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,17 @@ 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
+  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

From 0c3cd3fa5185717e0a0f3927df01a36bb18c7a97 Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Sun, 14 Jun 2026 09:33:50 +0100
Subject: [PATCH 2/9] Fix

---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 15e464eae4914c..1ebdf677a854f2 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -464,6 +464,7 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
 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]
 

From f32495a58c75949e03253ac794ebaa5eb949e291 Mon Sep 17 00:00:00 2001
From: ajirving <29164966+ajirving@users.noreply.github.com>
Date: Sun, 14 Jun 2026 15:27:27 +0100
Subject: [PATCH 3/9] Whitespace fix from code review

Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 1ebdf677a854f2..561de74a946a85 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -463,7 +463,7 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
 
 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
+    HasProd (fun x ↦ (f x)⁻¹) a⁻¹ := by
   unfold HasProd
   convert Filter.Tendsto.inv₀ h ha
   rw [Finset.prod_inv_distrib]

From cf8b53ebcceb465aa64efee67302b3133b2a4dfb Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Sun, 14 Jun 2026 15:32:39 +0100
Subject: [PATCH 4/9] Generalise summation filter

---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 561de74a946a85..7d2ad3afee21f5 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -419,6 +419,7 @@ end IsTopologicalGroup
 section CommGroupWithZero
 variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K] [SeparatelyContinuousMul K]
   {f g : α → K}
+  {L : SummationFilter α}
 /-!
 ## Groups with a zero
 
@@ -462,16 +463,16 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
   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
+theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a L) (ha : a ≠ 0) :
+    HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L := 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
+    (hf : HasProd f a L) (hg : HasProd g b L) (hb : b ≠ 0) :
+    HasProd (fun x ↦ f x / g x) (a / b) L := by
   simp only [div_eq_mul_inv]
   exact hf.mul <| hg.inv₀ hb
 

From b2c7c90669912bcf1677de0de6903bfe629ba35f Mon Sep 17 00:00:00 2001
From: ajirving <29164966+ajirving@users.noreply.github.com>
Date: Fri, 10 Jul 2026 16:40:51 +0100
Subject: [PATCH 5/9] Extra newlines suggested by review

Co-authored-by: Hannah Scholz <70071345+scholzhannah@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 7d2ad3afee21f5..87748c39912df1 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -417,9 +417,10 @@ theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β) :=
 end IsTopologicalGroup
 
 section CommGroupWithZero
+
 variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K] [SeparatelyContinuousMul K]
-  {f g : α → K}
-  {L : SummationFilter α}
+  {f g : α → K} {L : SummationFilter α}
+
 /-!
 ## Groups with a zero
 

From 9c9ffa5f0f69007aa07e2e8216a91e4fa1a676a9 Mon Sep 17 00:00:00 2001
From: ajirving <29164966+ajirving@users.noreply.github.com>
Date: Fri, 10 Jul 2026 16:41:15 +0100
Subject: [PATCH 6/9] Suggestion from code review

Co-authored-by: Hannah Scholz <70071345+scholzhannah@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 87748c39912df1..348758a5515b58 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -466,9 +466,8 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
 omit [SeparatelyContinuousMul K] in
 theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a L) (ha : a ≠ 0) :
     HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L := by
-  unfold HasProd
-  convert Filter.Tendsto.inv₀ h ha
-  rw [Finset.prod_inv_distrib]
+  simp_rw [HasProd, Finset.prod_inv_distrib]
+  exact Tendsto.inv₀ h ha
 
 omit [SeparatelyContinuousMul K] in
 theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}

From 1a4a249df31c93ffec461649fbfba008f068a098 Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Fri, 10 Jul 2026 17:01:54 +0100
Subject: [PATCH 7/9] Empty to rerun jobs


From 3c6d1ffe9ec28d643a3b9b991edcc2cb64898319 Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Wed, 22 Jul 2026 17:44:55 +0100
Subject: [PATCH 8/9] Multipliable and tprod variants

---
 .../Topology/Algebra/InfiniteSum/Group.lean   | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 9f8c5857ac5590..361b5b0d67b851 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -468,6 +468,17 @@ theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a L) (ha : a
   simp_rw [HasProd, Finset.prod_inv_distrib]
   exact Tendsto.inv₀ h ha
 
+omit [SeparatelyContinuousMul K] in
+theorem Multipliable.inv₀ [ContinuousInv₀ K] (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
+    Multipliable (fun x ↦ (f x)⁻¹) L :=
+  h.hasProd.inv₀ ne_zero|>.multipliable
+
+omit [SeparatelyContinuousMul K] in
+theorem Multipliable.tprod_inv₀ [ContinuousInv₀ K] [T2Space K] [L.NeBot]
+    (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
+    ∏'[L] x, (f x)⁻¹ = (∏'[L] x, f x )⁻¹ :=
+  h.hasProd.inv₀ ne_zero|>.tprod_eq
+
 omit [SeparatelyContinuousMul K] in
 theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}
     (hf : HasProd f a L) (hg : HasProd g b L) (hb : b ≠ 0) :
@@ -475,4 +486,16 @@ theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}
   simp only [div_eq_mul_inv]
   exact hf.mul <| hg.inv₀ hb
 
+omit [SeparatelyContinuousMul K] in
+theorem Multipliable.div₀ [ContinuousInv₀ K] [ContinuousMul K]
+    (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
+    Multipliable (fun x ↦ f x / g x) L :=
+  hf.hasProd.div₀ hg.hasProd ne_zero|>.multipliable
+
+omit [SeparatelyContinuousMul K] in
+theorem Multipliable.tprod_div₀ [ContinuousInv₀ K] [ContinuousMul K] [T2Space K] [L.NeBot]
+    (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
+    (∏'[L] x, f x / g x) = (∏'[L] x, f x) / (∏'[L] x, g x) :=
+  hf.hasProd.div₀ hg.hasProd ne_zero|>.tprod_eq
+
 end CommGroupWithZero

From 687b024da5e0c96eded63a0d4fee262b9e38548d Mon Sep 17 00:00:00 2001
From: Alastair Irving <29164966+ajirving@users.noreply.github.com>
Date: Thu, 23 Jul 2026 09:10:01 +0100
Subject: [PATCH 9/9] Use a section to avoid repeated omit

---
 Mathlib/Topology/Algebra/InfiniteSum/Group.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 361b5b0d67b851..089c65ef760b25 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -417,7 +417,7 @@ end IsTopologicalGroup
 
 section CommGroupWithZero
 
-variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K] [SeparatelyContinuousMul K]
+variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K]
   {f g : α → K} {L : SummationFilter α}
 
 /-!
@@ -427,6 +427,10 @@ These lemmas apply to a `CommGroupWithZero`; the most familiar case is when `K`
 are specific to the product setting and do not have a sensible additive analogue.
 -/
 
+section SeparatelyContinuousMul
+
+variable [SeparatelyContinuousMul K]
+
 open Finset in
 lemma HasProd.congr_cofinite₀ {c : K} (hc : HasProd f c) {s : Finset α}
     (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
@@ -462,37 +466,33 @@ 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
+end SeparatelyContinuousMul
+
 theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a L) (ha : a ≠ 0) :
     HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L := by
   simp_rw [HasProd, Finset.prod_inv_distrib]
   exact Tendsto.inv₀ h ha
 
-omit [SeparatelyContinuousMul K] in
 theorem Multipliable.inv₀ [ContinuousInv₀ K] (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
     Multipliable (fun x ↦ (f x)⁻¹) L :=
   h.hasProd.inv₀ ne_zero|>.multipliable
 
-omit [SeparatelyContinuousMul K] in
 theorem Multipliable.tprod_inv₀ [ContinuousInv₀ K] [T2Space K] [L.NeBot]
     (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
     ∏'[L] x, (f x)⁻¹ = (∏'[L] x, f x )⁻¹ :=
   h.hasProd.inv₀ ne_zero|>.tprod_eq
 
-omit [SeparatelyContinuousMul K] in
 theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}
     (hf : HasProd f a L) (hg : HasProd g b L) (hb : b ≠ 0) :
     HasProd (fun x ↦ f x / g x) (a / b) L := by
   simp only [div_eq_mul_inv]
   exact hf.mul <| hg.inv₀ hb
 
-omit [SeparatelyContinuousMul K] in
 theorem Multipliable.div₀ [ContinuousInv₀ K] [ContinuousMul K]
     (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
     Multipliable (fun x ↦ f x / g x) L :=
   hf.hasProd.div₀ hg.hasProd ne_zero|>.multipliable
 
-omit [SeparatelyContinuousMul K] in
 theorem Multipliable.tprod_div₀ [ContinuousInv₀ K] [ContinuousMul K] [T2Space K] [L.NeBot]
     (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
     (∏'[L] x, f x / g x) = (∏'[L] x, f x) / (∏'[L] x, g x) :=