coeff_scaleRoots_natDegree — Mathlib

English

Let p be a polynomial over a semiring R and s ∈ R. The coefficient of the top-degree term of scaleRoots(p, s) equals the leading coefficient of p. In particular, (scaleRoots p s).coeff(p.natDegree) = p.leadingCoeff.

Русский

Пусть p — многочлен над полем, и s ∈ R. Коэффициент при старшей степени в scaleRoots(p, s) равен ведущему коэффициенту p, то есть (scaleRoots p s).coeff(p.natDegree) = p.leadingCoeff.

LaTeX

$$$\operatorname{coeff}(\operatorname{scaleRoots}(p, s), \operatorname{natDegree}(p)) = \operatorname{leadingCoeff}(p)$$$

Lean4

theorem coeff_scaleRoots_natDegree (p : R[X]) (s : R) : (scaleRoots p s).coeff p.natDegree = p.leadingCoeff := by
  rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]

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