natDegree_pos_of_aeval_root — Mathlib

English

If p is a nonzero polynomial over R and its evaluation at some z in an algebra extension is zero, with an injective map from R to S, then the natural degree natDegree(p) is positive.

Русский

Если p не равен нулю и существует z в расширении, для которого p обнуляется, и соответствующее отображение из R в S инъективно, тогда natDegree(p) положительно.

LaTeX

$$$$ p \\neq 0 \\quad\\Rightarrow\\quad 0 < \\operatorname{natDegree}(p). $$$$

Lean4

theorem natDegree_pos_of_aeval_root [Algebra R S] {p : R[X]} (hp : p ≠ 0) {z : S} (hz : aeval z p = 0)
    (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) : 0 < p.natDegree :=
  natDegree_pos_of_eval₂_root hp (algebraMap R S) hz inj

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