degree_pos_of_aeval_root — Mathlib

English

If p ≠ 0 and there exists z with aeval z p = 0, under suitable injectivity assumptions, then deg(p) > 0.

Русский

Если p ≠ 0 и существует z с aeval z p = 0, при условии некоторые инъекции, то deg(p) > 0.

LaTeX

$$$$ p \\neq 0 \\quad\\Rightarrow\\quad 0 < p.degree. $$$$

Lean4

theorem degree_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.degree :=
  natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_aeval_root hp hz inj)

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