English
The power-series family is additive in the coefficients: powerSeries x (f+g) = powerSeries x f + powerSeries x g.
Русский
Семейство степенных рядов по коэффициентам аддитивно: powerSeries x (f+g) = powerSeries x f + powerSeries x g.
LaTeX
$$powerSeriesFamily x (f + g) = powerSeriesFamily x f + powerSeriesFamily x g$$
Lean4
/-- The `R`-algebra homomorphism from `R[[X]]` to `HahnSeries Γ R` given by sending the power series
variable `X` to a positive order element `x` and extending to infinite sums. -/
@[simps]
def heval : PowerSeries R →ₐ[R] HahnSeries Γ R
where
toFun f := (powerSeriesFamily x f).hsum
map_one' := by
simp only [hsum, smulFamily_toFun, coeff_one, powers_toFun, ite_smul, one_smul, zero_smul]
ext g
simp only
rw [finsum_eq_single _ (0 : ℕ) (fun n hn => by simp [hn])]
simp
map_mul' a b := by simp only [← hsum_mul, hsum_powerSeriesFamily_mul]
map_zero' := by
simp only [hsum, smulFamily_toFun, map_zero, zero_smul, coeff_zero, finsum_zero, mk_eq_zero, Pi.zero_def]
map_add' a b := by simp only [powerSeriesFamily_add, hsum_add]
commutes'
r := by
simp only [algebraMap_eq]
ext g
simp only [coeff_hsum, smulFamily_toFun, coeff_C, powers_toFun, ite_smul, zero_smul]
rw [finsum_eq_single _ 0 fun n hn => by simp [hn]]
by_cases hg : g = 0 <;> simp [hg, Algebra.algebraMap_eq_smul_one]
