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