coeff_rescale — Mathlib

English

The n-th coefficient of rescale a applied to f is a^n times the n-th coefficient of f.

Русский

n-ый коэффициент преобразования масштабирования равен a^n помножить на n-ый коэффициент f.

LaTeX

$$$\operatorname{coeff}_n(\mathrm{rescale}\, a\, f) = a^{n} \cdot \operatorname{coeff}_n f$$$

Lean4

@[simp]
theorem coeff_rescale (f : R⟦X⟧) (a : R) (n : ℕ) : coeff n (rescale a f) = a ^ n * coeff n f :=
  coeff_mk n (fun n ↦ a ^ n * coeff n f)

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