no goals
ι : Type u_2
κ : Type ?u.21514
R : Type ?u.21517
α : Type u_1
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
⊢ (∑' (x : ι), f x / a) = (∑' (x : ι), f x) / a
simpa only [div_eq_mul_inv] using tsum_mul_right