English
Rescale of a product of index functions equals the composition of rescalings: rescale(a·b) = (rescale b) ∘ (rescale a).
Русский
Масштабирование произведения функций-индексов равно композиции масштабирования: rescale(a·b) = (rescale b) ∘ (rescale a).
LaTeX
$$$\operatorname{rescale}(a \cdot b) = (\operatorname{rescale} b) \circ (\operatorname{rescale} a)$$$
Lean4
@[simp]
theorem coeff_rescale (f : MvPowerSeries σ R) (a : σ → R) (n : σ →₀ ℕ) :
coeff n (rescale a f) = (n.prod fun s m ↦ a s ^ m) * f.coeff n := by simp [rescale, coeff_apply]