exists_aeval_eq_zero — Mathlib

English

Let K be a separably closed field with an algebra structure over k. For any p ∈ k[X] with deg p ≠ 0 and p.Separable, there exists x ∈ K with aeval x p = 0.

Русский

Пусть K — сепарабельное замкнутое поле с алгебраической структурой над k. Для любого p ∈ k[X] deg p ≠ 0 и p.Separable существует x ∈ K такой, что aeval x p = 0.

LaTeX

$$∃ x ∈ K, aeval x p = 0$$

Lean4

theorem exists_aeval_eq_zero [IsSepClosed K] [Algebra k K] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
    ∃ x : K, aeval x p = 0 :=
  exists_eval₂_eq_zero (algebraMap k K) p hp hsep

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