English
Let f: α → ℝ and x ∈ ℝ. The HasSum of the real-valued series embedded into 𝕜 coincides with the HasSum of the original real-valued series: HasSum (a ↦ (f(a) : 𝕜)) x L iff HasSum f x L.
Русский
Пусть f: α → ℝ и x ∈ ℝ. Сумма ряда вещественных чисел, встроенная в 𝕜, существует тогда и только тогда, когда существует сумма самого ряда вещественных чисел: HasSum (a ↦ (f(a) : 𝕜)) x L эквивалично HasSum f x L.
LaTeX
$$$ HasSum\\bigl(a \\mapsto (f(a) : \\mathbb{K})\\bigr)\\, x\\;L \\;\\iff \\; HasSum\\; f\\; x\\; L $$$
Lean4
@[simp, norm_cast]
theorem hasSum_ofReal {f : α → ℝ} {x : ℝ} : HasSum (fun x => (f x : 𝕜)) x L ↔ HasSum f x L :=
⟨fun h => by simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.hasSum h, ofRealCLM.hasSum⟩
