range_eval_eq_rootSet_minpoly — Mathlib

English

The set of values obtained by evaluating K→ₐ[F] A at x ranges exactly over the roots of the minimal polynomial of x over F in A.

Русский

Множество значений, получаемых применением алгебраических гомоморфизмов из K в A к x, совпадает с корнями минимального многочлена x над F в A.

LaTeX

$$$\\{ ψ(x) : ψ : K \\to_A F A \\} = \\text{rootSet}_A(F, x).$$

Lean4

/-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
  of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
  the roots in `A` of the minimal polynomial of `x` over `F`. -/
theorem range_eval_eq_rootSet_minpoly [IsAlgClosed A] (x : K) :
    (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A :=
  range_eval_eq_rootSet_minpoly_of_splits A (fun _ ↦ IsAlgClosed.splits_codomain _) x

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