ι : Type ?u.33257
κ : Type ?u.33260
R : Type ?u.33263
α : 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 => ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
ι : Type ?u.33257
κ : Type ?u.33260
R : Type ?u.33263
α : 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 => ∑ k in range (n + 1), f k * g (n - k)
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
no goals
ι : Type ?u.33257
κ : Type ?u.33260
R : Type ?u.33263
α : 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 => ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
exact summable_sum_mul_antidiagonal_of_summable_mul h