no goals
ι : Type u_2
κ : Type ?u.15580
R : Type ?u.15583
α : Type u_1
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
⊢ (Summable fun i => f i / a) ↔ Summable f
simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)