support_scaleRoots_le — Mathlib

English

The support of scaleRoots(p, s) is contained in the support of p; i.e., no new nonzero coefficients are created by scaling the roots.

Русский

Поддержка scaleRoots(p, s) содержится в поддержке p; новые ненулевые коэффициенты не возникают при масштабировании корней.

LaTeX

$$$\operatorname{support}(\operatorname{scaleRoots}(p, s)) \subseteq \operatorname{support}(p)$$$

Lean4

theorem support_scaleRoots_le (p : R[X]) (s : R) : (scaleRoots p s).support ≤ p.support :=
  by
  intro
  simpa using left_ne_zero_of_mul

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