English
Let A, B be domains and p ∈ A[X], f: A →+* B injective. Then card p.roots ≤ card (p.map f).roots.
Русский
Пусть A, B — области и p ∈ A[X], f: A →+* B инъективен. Тогда card(p.roots) ≤ card((p.map f).roots).
LaTeX
$$$\forall {A B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} {f : A \to+* B},\; Function.Injective (RingHom.instFunLike.coe f) \Rightarrow \operatorname{card} p.roots \le \operatorname{card} (p.map f).roots$$$
Lean4
theorem card_roots_le_map_of_injective [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (hf : Function.Injective f) :
Multiset.card p.roots ≤ Multiset.card (p.map f).roots :=
by
by_cases hp0 : p = 0
· simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]
exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)
