feat(Topology/Algebra/InfiniteSum/NatInt): hasProd versions of ℕ+/ℕ transfer lemmas (leanprover-community#41502)

The `PNat` section of `Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean` provides `Multipliable` and `tprod` lemmas for transferring infinite products between `ℕ+` and `ℕ`, but not `HasProd` lemmas. This PR completes this gap with:

* `hasProd_pnat_iff_hasProd_succ`: `HasProd (fun n : ℕ+ ↦ f n) m ↔ HasProd (fun n : ℕ ↦ f (n + 1)) m`, the `HasProd` counterpart of the existing `multipliable_pnat_iff_multipliable_succ`
* `hasProd_pnat_iff`: in a topological group, `HasProd (fun n : ℕ+ ↦ f n) g ↔ HasProd f (g * f 0)`, the counterpart of `multipliable_pnat_iff_multipliable_nat`
* `tprod_pnat_eq_tprod_of_eq_one`: if `f 0 = 1`, then `∏' n : ℕ+, f n = ∏' n, f n`. Unlike `tprod_zero_pnat_eq_tprod_nat`, this requires no multipliability hypothesis (and no group structure or `T2Space`)

**Motivation**: the additive versions (`hasSum_pnat_iff`, `tsum_pnat_eq_tsum_of_eq_zero`, ...) replace
three private lemmas in the [FLT project](https://github.com/ImperialCollegeLondon/FLT) (`hasSum_nat_of_pnat_add`, `hasSum_pnat_of_nat`, `tsum_pnat_of_zero`), each of which becomes a one-line application, stated there for `ℂ` only.

**AI Disclosure**: original code in FLT was written by William Coram and Samuel Yin with the assistance of Claude. It was later cleaned up using Codex.

Co-authored-by: William Coram
Co-authored-by: Samuel Yin

Author: pepamontero

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -541,10 +541,28 @@ lemma multipliable_pnat_iff_multipliable_nat [TopologicalSpace G] [IsTopological
     {f : ℕ → G} : Multipliable (fun n : ℕ+ ↦ f n) ↔ Multipliable f := by
   rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]
 
+@[to_additive]
+theorem hasProd_pnat_iff_hasProd_succ {f : ℕ → M} :
+    HasProd (fun x : ℕ+ ↦ f x) m ↔ HasProd (fun x : ℕ ↦ f (x + 1)) m :=
+  Equiv.pnatEquivNat.symm.hasProd_iff.symm
+
+@[to_additive]
+theorem hasProd_pnat_iff [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} {a : G} :
+    HasProd (fun x : ℕ+ ↦ f x) a ↔ HasProd f (a * f 0) := by
+  simp [hasProd_pnat_iff_hasProd_succ, hasProd_nat_add_iff]
+
 @[to_additive]
 theorem tprod_pnat_eq_tprod_succ {f : ℕ → M} : ∏' n : ℕ+, f n = ∏' n, f (n + 1) :=
   (Equiv.pnatEquivNat.symm.tprod_eq _).symm
 
+@[to_additive]
+theorem tprod_pnat_eq_tprod_of_eq_one {f : ℕ → M} (hf : f 0 = 1) :
+    ∏' n : ℕ+, f n = ∏' n : ℕ, f n :=
+  PNat.coe_injective.tprod_eq fun n hn ↦ by
+    rcases Nat.eq_zero_or_pos n with rfl | h
+    · exact absurd hf hn
+    · exact ⟨⟨n, h⟩, rfl⟩
+
 @[to_additive]
 lemma tprod_zero_pnat_eq_tprod_nat [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
     {f : ℕ → G} (hf : Multipliable f) :