scaleRoots_ne_zero — Mathlib

English

If p ≠ 0, then scaleRoots(p, s) ≠ 0 for any s ∈ R.

Русский

Если p ≠ 0, то scaleRoots(p, s) ≠ 0 для любого s ∈ R.

LaTeX

$$$p \neq 0 \;\Rightarrow\; \operatorname{scaleRoots}(p, s) \neq 0$$$

Lean4

theorem scaleRoots_ne_zero {p : R[X]} (hp : p ≠ 0) (s : R) : scaleRoots p s ≠ 0 :=
  by
  intro h
  have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
  have : (scaleRoots p s).coeff p.natDegree = 0 := congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree
  rw [coeff_scaleRoots_natDegree] at this
  contradiction

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