English
Let p ≠ 0 be a polynomial over a domain and s a multiset of elements of the base ring. The product ∏ (X − a) over a ∈ s divides p if and only if s is contained as a submultiset of the roots of p.
Русский
Пусть p ≠ 0 — многочлен над осн. кольцом и s — мульти-множество элементов. Произведение по (X − a) делит p тогда и только тогда, когда s входит как подмножество корней p.
LaTeX
$$$p \neq 0 \;\Rightarrow\; \Big(\prod_{a \in s} (X - C a)\Big) \;|\; p \;\text{ iff }\; s \le p.x\text{ roots}$$$
Lean4
/-- A Galois connection. -/
theorem _root_.Multiset.prod_X_sub_C_dvd_iff_le_roots {p : R[X]} (hp : p ≠ 0) (s : Multiset R) :
(s.map fun a => X - C a).prod ∣ p ↔ s ≤ p.roots := by
classical
exact
⟨fun h =>
Multiset.le_iff_count.2 fun r =>
by
rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
fun h => (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩
