scaleRoots_zero — Mathlib

English

The scaleRoots of a polynomial by 0 equals the leading coefficient times X to the natDegree.

Русский

ScaleRoots на 0 равен ведущему коэффициенту крат X^{natDegree}.

LaTeX

$$$\operatorname{scaleRoots}(p, 0) = \operatorname{leadingCoeff}(p) \cdot X^{\operatorname{natDegree}}(p)$$$

Lean4

@[simp]
theorem scaleRoots_zero (p : R[X]) : p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree :=
  by
  ext n
  simp only [coeff_scaleRoots, tsub_eq_zero_iff_le, zero_pow_eq, mul_ite, mul_one, mul_zero, coeff_smul, coeff_X_pow,
    smul_eq_mul]
  split_ifs with h₁ h₂ h₂
  · subst h₂; rfl
  · exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))
  · exact (h₁ h₂.ge).elim
  · rfl

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