English
Let A, B be domains and p ∈ A[X]. Let f: A →* B be a ring hom. If p.map f ≠ 0, then the image of the root multiset of p under f is a submultiset of the root multiset of p.map f; equivalently, p.roots.map f ≤ (p.map f).roots.
Русский
Пусть A, B — области, p ∈ A[X], f: A →* B — кольцевой гомоморфизм. Если p.map f ≠ 0, то образ мультимножества корней p под f является подмультимножеством корней p.map f; то есть p.roots.map f ≤ (p.map f).roots.
LaTeX
$$$\forall {A,B} [\text{IsDomain } A] [\text{IsDomain } B] {p : A[X]} {f : A \to+* B}\; (h : p.map f \neq 0) \Rightarrow p.roots.map f \le (p.map f).roots$$$
Lean4
theorem map_roots_le [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
p.roots.map f ≤ (p.map f).roots := by
classical
exact
Multiset.le_iff_count.2 fun b => by
rw [count_roots]
apply count_map_roots h
