English
For a ∈ R, the rescale map on PowerSeries R is given by (rescale a f)(X) = ∑_{n≥0} a^n (coeff_n f) X^n.
Русский
Для a ∈ R отображение повторного масштабирования степенных рядов задано как (rescale a f)(X) = ∑_{n≥0} a^n (coeff_n f) X^n.
LaTeX
$$$(\mathrm{rescale}\, a\, f) = \sum_{n\ge 0} a^{n} \operatorname{coeff}_n(f) X^{n}$$$
Lean4
/-- The ring homomorphism taking a power series `f(X)` to `f(aX)`. -/
noncomputable def rescale (a : R) : R⟦X⟧ →+* R⟦X⟧
where
toFun f := PowerSeries.mk fun n => a ^ n * PowerSeries.coeff n f
map_zero' := by
ext
simp only [LinearMap.map_zero, PowerSeries.coeff_mk, mul_zero]
map_one' := by
ext1
simp only [mul_boole, PowerSeries.coeff_mk, PowerSeries.coeff_one]
split_ifs with h
· rw [h, pow_zero a]
rfl
map_add' := by
intros
ext
dsimp only
exact mul_add _ _ _
map_mul' f
g := by
ext
rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]
apply sum_congr rfl
simp only [coeff_mk, Prod.forall, mem_antidiagonal]
intro b c H
rw [← H, pow_add, mul_mul_mul_comm]
