feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)

Add some basic results about tsums indexed by pnat.



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Author: CBirkbeck

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -514,3 +514,16 @@ lemma multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} :
 end UniformGroup
 
 end Int
+
+section pnat
+
+@[to_additive]
+theorem pnat_multipliable_iff_multipliable_succ {α : Type*} [TopologicalSpace α] [CommMonoid α]
+    {f : ℕ → α} : Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) :=
+  Equiv.pnatEquivNat.symm.multipliable_iff.symm
+
+@[to_additive]
+theorem tprod_pnat_eq_tprod_succ {α : Type*} [TopologicalSpace α] [CommMonoid α] (f : ℕ → α) :
+    ∏' n : ℕ+, f n = ∏' n, f (n + 1) := (Equiv.pnatEquivNat.symm.tprod_eq _).symm
+
+end pnat