isAlgebraic_of_mem_rootSet — Mathlib

English

If x ∈ p.rootSet A for some p ∈ R[X] and field A, then x is algebraic over R.

Русский

Если x принадлежит ROOT-множеству p в A, то x алгебраичен над R.

LaTeX

$$$ \forall {p : R[X]} {x : A}, x \in p.rootSet A \to IsAlgebraic R x $$$

Lean4

theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [CommRing R] [Field A] [Algebra R A] {p : R[X]} {x : A}
    (hx : x ∈ p.rootSet A) : IsAlgebraic R x :=
  ⟨p, ne_zero_of_mem_rootSet hx, aeval_eq_zero_of_mem_rootSet hx⟩

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