English
Let F be a subfield of K. If f ∈ F[X] is nonzero, splits over algebraMap F → F, and a root x of f.map F.subtype lies in K, then x ∈ F.
Русский
Пусть F ⊆ K. Если f ∈ F[X] ненулевой, распадается над отображением F, а некотрый корень x из f.map F.subtype принадлежит K, тогда x ∈ F.
LaTeX
$$$\\forall \\text{F : Subfield } K,\\; f : F[X],\\; f \\neq 0,\\; \\text{Splits }(\\mathrm{RingHom.id} F)\\; f\\Rightarrow \\forall x:\\ K,\\; (f.map F.subtype).\\IsRoot x \\Rightarrow x \\in F.$$$
Lean4
theorem mem_subfield_of_isRoot (F : Subfield K) {f : F[X]} (hnz : f ≠ 0) (hf : Splits (RingHom.id F) f) {x : K}
(hx : (f.map F.subtype).IsRoot x) : x ∈ F :=
by
obtain ⟨x, _, rfl⟩ := Multiset.mem_map.mp (roots_map F.subtype hf ▸ mem_roots'.mpr ⟨Polynomial.map_ne_zero hnz, hx⟩)
exact x.2
