restrictScalars — Mathlib

English

Restriction of scalars lowers the base field: if f is analytic within at 𝕜' then it is analytic within at 𝕜.

Русский

Сужение скаляров понижает базовое поле: если f аналитична внутри в 𝕜', то она аналитична внутри в 𝕜.

LaTeX

$$$\mathrm{AnalyticWithinAt}_{\mathbb{K}'}(f,s,z) \Rightarrow \mathrm{AnalyticWithinAt}_{\mathbb{K}}(f,s,z)$$$

Lean4

theorem restrictScalars (hf : HasFPowerSeriesWithinAt f p s x) : HasFPowerSeriesWithinAt f (p.restrictScalars 𝕜) s x :=
  by
  rcases hf with ⟨r, hr⟩
  exact ⟨r, hr.restrictScalars⟩

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