no goals
α : Type u_1
f : α → ℝ
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
simpa only using
  Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _)
    (continuous_algebraMap _ _) continuous_re coe_re