coeff_scaleRoots — Mathlib

English

The coefficient of scaleRoots(p,s) at index i equals the original coefficient p.i multiplied by s raised to the power (natDegree(p) − i).

Русский

Коэффициент scaleRoots(p,s) при индексе i равен коэффициенту p.i, умноженному на s, возведённому в степень (natDegree(p) − i).

LaTeX

$$$(\\mathrm{scaleRoots}\\; p\\; s)^{\\,\\text{coeff}}(i) = p.i \\cdot s^{(p.natDegree - i)}$$

Lean4

@[simp]
theorem coeff_scaleRoots (p : R[X]) (s : R) (i : ℕ) : (scaleRoots p s).coeff i = coeff p i * s ^ (p.natDegree - i) := by
  simp +contextual [scaleRoots, coeff_monomial]

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