English
Let p be a polynomial over K and F an intermediate field of L. Then p is a splitting field over F if and only if p splits over F and F equals the adjoin of the roots of p in L.
Русский
Пусть p — полином над K, и F — промежуточное поле L. Тогда p является полем развилки над F тогда и только тогда, когда p распадается над F и F совпадает с адъюнтом корней p в L.
LaTeX
$$$\\text{Polynomial.IsSplittingField } K F \\iff \\text{Polynomial.Splits}(\\text{algebraMap } K F) \\wedge F = \\operatorname{adjoin}_K(p.rootSet L)$$$
Lean4
theorem isSplittingField_iff : p.IsSplittingField K F ↔ p.Splits (algebraMap K F) ∧ F = adjoin K (p.rootSet L) :=
by
suffices _ → (Algebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
rw [← toSubalgebra_injective.eq_iff, adjoin_algebraic_toSubalgebra fun x ↦ isAlgebraic_of_mem_rootSet]
refine fun hp ↦ (adjoin_rootSet_eq_range hp F.val).symm.trans ?_
rw [← F.range_val, eq_comm]
