adjoin_rootSet_isSplittingField — Mathlib

English

If a polynomial p splits over K in L, then p is the splitting field of K with respect to the subfield adjoin K (p.rootSet L).

Русский

Если полином p распадается над K внутри L, то p является полем развилки для K относительно подполе, порождаемого адъюнтом корней p в L.

LaTeX

$$$\\text{Polynomial.Splits}(\\text{algebraMap } K L) \\Rightarrow \\text{Polynomial.IsSplittingField } K(\\operatorname{adjoin}_K(p.rootSet L))$$$

Lean4

theorem adjoin_rootSet_isSplittingField (hp : p.Splits (algebraMap K L)) :
    p.IsSplittingField K (adjoin K (p.rootSet L)) :=
  isSplittingField_iff.mpr ⟨splits_of_splits hp fun _ hx ↦ subset_adjoin K (p.rootSet L) hx, rfl⟩

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