English
For a polynomial p ∈ A[x] and a map f: A →+* B with p.map f ≠ 0, the count of a given b in the image of roots is at most the rootMultiplicity of b in p.map f.
Русский
Для многочлена p ∈ A[x] и отображения f: A →+* B с p.map f ≠ 0, число объектов b в образе корней не превосходит кратности корня b в p.map f.
LaTeX
$$(p.roots.map f).count b ≤ rootMultiplicity(b, p.map f)$$
Lean4
theorem count_map_roots [IsDomain A] [DecidableEq B] {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0) (b : B) :
(p.roots.map f).count b ≤ rootMultiplicity b (p.map f) :=
by
rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ← Multiset.map_replicate fun a => X - C a]
rw [← Multiset.filter_eq]
refine (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_
convert Polynomial.map_dvd f p.prod_multiset_X_sub_C_dvd
simp only [Polynomial.map_multiset_prod, Multiset.map_map, Function.comp_apply, Polynomial.map_sub, map_X, map_C]
