English
Let A, B be domains and p ∈ A[X]. If f: A →* B is injective, then p.roots.map f ≤ (p.map f).roots. (If p = 0 the statement is trivial.)
Русский
Пусть A, B — области и p ∈ A[X]. Для инъективного f: A →* B верно p.roots.map f ≤ (p.map f).roots (в случае p = 0 утверждение тривиально).
LaTeX
$$$\forall {A,B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} {f : A \to+* B},\; (hf : Function.Injective f) \Rightarrow p.roots.map f \le (p.map f).roots$$$
Lean4
theorem map_roots_le_of_injective [IsDomain A] [IsDomain B] (p : A[X]) {f : A →+* B} (hf : Function.Injective f) :
p.roots.map f ≤ (p.map f).roots := by
by_cases hp0 : p = 0
· simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]
exact map_roots_le ((Polynomial.map_ne_zero_iff hf).mpr hp0)
