English
Restriction of scalars preserves HasFPowerSeriesWithinOnBall: a power series within on a ball remains valid after restricting scalars.
Русский
Сужение скаляров сохраняет HasFPowerSeriesWithinOnBall: степенной ряд в шаре сохраняется после ограничения скаляров.
LaTeX
$$$\text{HasFPowerSeriesWithinOnBall}(f,p,s,x,r) \Rightarrow \text{HasFPowerSeriesWithinOnBall}(f,p\!\restrictionScalars\;\mathbb{K},s,x,r)$$$
Lean4
theorem restrictScalars (hf : HasFPowerSeriesWithinOnBall f p s x r) :
HasFPowerSeriesWithinOnBall f (p.restrictScalars 𝕜) s x r :=
⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩