English
Scaling the coefficients of a power series corresponds to scaling the Hahn series family by the scalar via the zero term, i.e., powerSeriesFamily x (r • f) = (single 0 r) • powerSeriesFamily x f.
Русский
Умножение коэффициентов степенного ряда на скаляра отражается на семействе степенных рядов Hahn через нулевой элемент.
LaTeX
$$powerSeriesFamily x (r • f) = HahnSeries.single (0 : Γ) r • powerSeriesFamily x f$$
Lean4
theorem heval_C (r : R) : heval x (C r) = r • 1 := by
ext g
simp only [heval_apply, coeff_hsum, smulFamily_toFun, powers_toFun, HahnSeries.coeff_smul, HahnSeries.coeff_one,
smul_eq_mul, mul_ite, mul_one, mul_zero]
rw [finsum_eq_single _ 0 (fun n hn ↦ by simp [coeff_ne_zero_C hn])]
by_cases hg : g = 0 <;> simp
