[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): hasProd versions of ℕ+/ℕ transfer lemmas#41502

pepamontero wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

pepamontero:NatInt-LogosWSpepamontero/mathlib4:NatInt-LogosWSCopy head branch name to clipboard