rescale_mk — Mathlib

English

Rescale acts on the mk construction by rescaling each coordinate: rescale a (mk f) = mk (n ↦ a^n f(n)).

Русский

При применении масштаба к конструктору mk каждый коэффициент масштабируется: rescale a (mk f) = mk (n ↦ a^n f(n)).

LaTeX

$$$\mathrm{rescale}\, a\, (\mathrm{mk}\, f) = \mathrm{mk}\, (n \mapsto a^{n} \cdot f(n))$$$

Lean4

theorem rescale_mk (f : ℕ → R) (a : R) : rescale a (mk f) = mk fun n : ℕ => a ^ n * f n :=
  by
  ext
  rw [coeff_rescale, coeff_mk, coeff_mk]

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