English
Let f be a polynomial over K and s a multiset of elements of L. If map i f equals a constant times a product over (X - a) for a in s, then f splits over i.
Русский
Пусть f ∈ K[X], s — мультисет элементов L. Если f.map i можно записать как C(i f.leadingCoeff) · ∏_{a∈s}(X - C a), то f распадается через i.
LaTeX
$$$\forall f:K[X],\forall s:Multiset\ L, f.map\ i = C(i f.leadingCoeff) \cdot (s.map (\lambda a. X - C a)).prod \Rightarrow Splits\, i\, f$$$
Lean4
theorem splits_of_exists_multiset {f : K[X]} {s : Multiset L}
(hs : f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod) : Splits i f :=
letI := Classical.decEq K
if hf0 : f = 0 then hf0.symm ▸ splits_zero i
else
Or.inr fun {p} hp hdp => by
rw [irreducible_iff_prime] at hp
rw [hs, ← Multiset.prod_toList] at hdp
obtain hd | hd := hp.2.2 _ _ hdp
· refine (hp.2.1 <| isUnit_of_dvd_unit hd ?_).elim
exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)
· obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd
obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)
rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]
exact degree_X_sub_C a
