coeff_rescale — Mathlib

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]

Похожие утверждения