exists_eval₂_eq_zero — Mathlib

English

For separable p ∈ k[X], there exists x ∈ K such that p.eval₂ f x = 0.

Русский

Для сепарабельного p ∈ k[X] существует x ∈ K такой, что p.eval₂ f x = 0.

LaTeX

$$∃ x: p.eval₂ f x = 0$$

Lean4

theorem exists_eval₂_eq_zero [IsSepClosed K] (f : k →+* K) (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
    ∃ x, p.eval₂ f x = 0 :=
  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective f.injective]) (Separable.map hsep)
  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩

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