restrictScalars — Mathlib

English

Restriction of scalars preserves HasFPowerSeriesOnBall: the series remains valid after restricting scalars.

Русский

Сужение скаляров сохраняет HasFPowerSeriesOnBall: ряд остается действительным после ограничения скаляров.

LaTeX

$$$\text{HasFPowerSeriesOnBall}(f,p,x,r) \Rightarrow \text{HasFPowerSeriesOnBall}(f,p\!\restrictionScalars\;\mathbb{K},x,r)$$$

Lean4

theorem restrictScalars (hf : HasFPowerSeriesOnBall f p x r) : HasFPowerSeriesOnBall f (p.restrictScalars 𝕜) x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

Похожие утверждения