ι : Type ?u.27646
κ : Type ?u.27649
R : Type ?u.27652
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
ι : Type ?u.27646
κ : Type ?u.27649
R : Type ?u.27652
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
ι : Type ?u.27646
κ : Type ?u.27649
R : Type ?u.27652
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun x => ∑' (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
ι : Type ?u.27646
κ : Type ?u.27649
R : Type ?u.27652
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
no goals
ι : Type ?u.27646
κ : Type ?u.27649
R : Type ?u.27652
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun x => ∑' (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
exact h.sigma' fun n => (hasSum_fintype _).summable