English
The coefficient of index n in the rescaled f equals (n.prod a^m) times the original coefficient: coeff n (rescale a f) = (n.prod fun s m => a s^m) · coeff n f.
Русский
Коэффициент при индексе n в масштабированном f равен произведению по всем s и m степеней a s, умноженным на исходный коэффициент: coeff n (rescale a f) = (n.prod a^m) · coeff n f.
LaTeX
$$$\operatorname{coeff}_n(\operatorname{rescale} a f) = \Big(\prod_{s} a(s)^{m}\Big) \cdot \operatorname{coeff}_n(f)$$$
Lean4
@[simp]
theorem rescale_zero : (rescale 0 : MvPowerSeries σ R →+* MvPowerSeries σ R) = C.comp constantCoeff := by
classical
ext x n
simp [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk, coeff_C]
split_ifs with h
· simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
· simp only [coeff_apply]
convert zero_mul _
simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
obtain ⟨s, h⟩ := h
simp only [Finsupp.prod]
apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
simpa using h
