algebraicClosure — Mathlib

English

If a polynomial splits in E, then it splits in the relative algebraic closure of F in E as well.

Русский

Если многочлен распадается в E, то он распадается и в относительном алгебраическом замыкании F в E.

LaTeX

$$$ p \\text{ splits in } E \\Rightarrow p \\text{ splits in } \\operatorname{algebraicClosure}_F(E) $$$

Lean4

/-- Let `E / F` be a field extension. If a polynomial `p`
splits in `E`, then it splits in the relative algebraic closure of `F` in `E` already.
-/
theorem algebraicClosure {p : F[X]} (h : p.Splits (algebraMap F E)) : p.Splits (algebraMap F (algebraicClosure F E)) :=
  splits_of_splits h fun _ hx ↦ (isAlgebraic_of_mem_rootSet hx).isIntegral

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