English
For any filter L and any f: α → ℝ, Summable (fun a => (f a : ℍ)) L is equivalent to Summable f L.
Русский
Для любого фильтра L и любого f: α → ℝ, суммация по coe сохраняется: Summable (λ a, (f a) : ℍ) L эквивалентно Summable f L.
LaTeX
$$$\operatorname{Summable}(\lambda a, (f a) : \mathbb{H})\, L \iff \operatorname{Summable}(f)\, L$$$
Lean4
@[simp, norm_cast]
theorem summable_coe {f : α → ℝ} : (Summable (fun a => (f a : ℍ)) L) ↔ Summable f L := by
simpa only using
Summable.map_iff_of_leftInverse (algebraMap ℝ ℍ) (show ℍ →ₗ[ℝ] ℝ from QuaternionAlgebra.reₗ _ _ _)
(continuous_algebraMap _ _) continuous_re re_coe