English
Rescaling by a and then substituting is the same as substituting by a X and then applying rescale.
Русский
Масштабирование по a затем подстановка эквивалентны подстановке по a·X затем масштабированию.
LaTeX
$$$\operatorname{rescale}(a) f = \operatorname{subst}(a \cdot X) f$$$
Lean4
/-- Rescaling a homogeneous power series -/
theorem rescale_homogeneous_eq_smul {n : ℕ} {r : R} {f : MvPowerSeries σ R} (hf : ∀ d ∈ f.support, d.degree = n) :
MvPowerSeries.rescale (Function.const σ r) f = r ^ n • f :=
by
ext e
simp only [MvPowerSeries.coeff_rescale, map_smul, Finsupp.prod, Function.const_apply, Finset.prod_pow_eq_pow_sum,
smul_eq_mul]
by_cases he : e ∈ f.support
· rw [← hf e he, Finsupp.degree]
· simp only [Function.mem_support, ne_eq, not_not] at he
simp [he, mul_zero, coeff_apply]