English
Let A, B be domains and p ∈ A[X], f: A →+* B with p.map f ≠ 0. Then the number of roots of p (counted with multiplicity) does not exceed the number of roots of p.map f.
Русский
Пусть A, B — области и p ∈ A[X], f: A →+* B так, что p.map f ≠ 0. Тогда число корней p (с учётом кратности) не превосходит число корней p.map f.
LaTeX
$$$\forall {A B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} {f : A \to+* B},\; (h : p.map f \neq 0) \Rightarrow \operatorname{card} p.roots \le \operatorname{card} (p.map f).roots$$$
Lean4
theorem card_roots_le_map [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
Multiset.card p.roots ≤ Multiset.card (p.map f).roots :=
by
rw [← p.roots.card_map f]
exact Multiset.card_le_card (map_roots_le h)
