English
If f is injective and the root multiset of p has cardinality equal to natDegree of p, then mapping roots commutes with map p: p.roots.map f = (p.map f).roots.
Русский
Если f инъективен и множество корней p имеет кардинальность, равную natDegree p, то отображение корней через f коммутирует с отображением p: p.roots.map f = (p.map f).roots.
LaTeX
$$$\forall {A B} [\text{IsDomain } A] [\text{IsDomain } B] {p : Polynomial A} (f : A \to+* B) (hf : Function.Injective f) (hroots : p.roots.card = p.natDegree),\; p.roots.map f = (p.map f).roots$$$
Lean4
theorem roots_map_of_injective_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B}
(hf : Function.Injective f) (hroots : Multiset.card p.roots = p.natDegree) : p.roots.map f = (p.map f).roots :=
by
apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
simpa only [Multiset.card_map, hroots] using (card_roots' _).trans natDegree_map_le
