natDegree_pos_of_eval₂_root — Mathlib

English

Let p ∈ R[X] be nonzero. If there exists a ring hom f: R → S and z ∈ S with eval₂ f z p = 0 and f is injective on R, then natDegree p > 0.

Русский

Пусть p ∈ R[X] не равно нулю. Если существует однозначное кольцевое отображение f: R → S и элемент z ∈ S такой, что eval₂ f z p = 0 и f сохраняет нульовую инжекцию, то natDegree(p) > 0.

LaTeX

$$$p \neq 0 \; \land\; \exists f: R \to^+* S, z\in S\; (eval_2 f z p = 0) \Rightarrow 0 < \operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_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 < natDegree p :=
  lt_of_not_ge fun hlt => by
    have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
    rw [A, eval₂_C] at hz
    simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A
    exact hp A

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