degree_pos_of_eval₂_root — Mathlib

English

Let p be a nonzero polynomial and f a ring hom R → S with z ∈ S and eval₂ f z p = 0, under a zero-preserving injectivity condition, then degree p > 0.

Русский

Пусть p не равно нулю и f: R → S — кольцевое отображение с z ∈ S и eval₂ f z p = 0; при условии сохраняющей нуль инъективности выполняется deg p > 0.

LaTeX

$$$p \neq 0 \land eval_2 f z p = 0 \land (\forall x, f x = 0 \Rightarrow x = 0) \Rightarrow 0 < \deg(p)$$$

Lean4

theorem degree_pos_of_eval₂_root {p : R[X]} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : eval₂ f z p = 0)
    (inj : ∀ x : R, f x = 0 → x = 0) : 0 < degree p :=
  natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_eval₂_root hp f hz inj)

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