English
If h ∈ F[X] is separable, x ∈ F is a root of h, i maps F into K with h.map i splitting in K, and every root of h.map i equals i x, then h = C(leadingCoeff h) · (X − C x).
Русский
Если h ∈ F[X] раздельно, x ∈ F является корнем h, а отображение i: F →+* K удовлетворяет распаду h.map i в K и каждое корневое значение h.map i равно i x, то тогда h = C(leadingCoeff h) · (X − C x).
LaTeX
$$$ h.Separable \\land h.eval x = 0 \\land Splits i h \\land (\\forall y \\in (h.map i).roots, y = i x) \\Rightarrow h = C(leadingCoeff h) \\cdot (X - C x) $$$
Lean4
theorem eq_X_sub_C_of_separable_of_root_eq {x : F} {h : F[X]} (h_sep : h.Separable) (h_root : h.eval x = 0)
(h_splits : Splits i h) (h_roots : ∀ y ∈ (h.map i).roots, y = i x) : h = C (leadingCoeff h) * (X - C x) :=
by
have h_ne_zero : h ≠ 0 := by
rintro rfl
exact not_separable_zero h_sep
apply Polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits
apply Finset.mk.inj
· change _ = {i x}
rw [Finset.eq_singleton_iff_unique_mem]
constructor
· apply Finset.mem_mk.mpr
· rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]
rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]
exact RingHom.map_zero i
· exact nodup_roots (Separable.map h_sep)
· exact h_roots
