no goals
ι : Type u_2
κ : Type ?u.17050
R : Type ?u.17053
α : Type u_1
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ (∑' (x : ι), a * f x) = a * ∑' (x : ι), f x
simp [ha]
no goals
ι : Type u_2
κ : Type ?u.17050
R : Type ?u.17053
α : Type u_1
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ (∑' (x : ι), a * f x) = a * ∑' (x : ι), f x
rw [tsum_eq_zero_of_not_summable hf,
    tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]