English
Let i: F →+* K be a ring hom and f ∈ F[X] be separable and split by i. Then there exists a finite set s ⊆ K such that f.map i equals C(i f.leadingCoeff) times the product over a ∈ s of (X − C a).
Русский
Пусть i: F →+* K — гомоморфизм кольца и f ∈ F[X] раздельно и распадается по i. Тогда существует конечное множество s под K такое, что f.map i = C(i f.leadingCoeff) · ∏_{a∈s} (X − C a).
LaTeX
$$∃ s ∈ Finset K, f.map i = C (i f.leadingCoeff) * s.prod (λ a, X - C a)$$
Lean4
theorem exists_finset_of_splits (i : F →+* K) {f : F[X]} (sep : Separable f) (sp : Splits i f) :
∃ s : Finset K, f.map i = C (i f.leadingCoeff) * s.prod fun a : K => X - C a := by
classical
obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp
use s.toFinset
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]
apply nodup_of_separable_prod
apply Separable.of_mul_right
rw [← h]
exact sep.map
