R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ↑f
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ ↑Multiset.card (roots (map f p)) ≤ ↑Multiset.card (Multiset.map (↑f) (roots p))
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ↑f
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Multiset.map (↑f) (roots p) = roots (map f p)
apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ↑f
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ ↑Multiset.card (roots (map f p)) ≤ ↑Multiset.card (Multiset.map (↑f) (roots p))
simpa only [Multiset.card_map, hroots] using (card_roots' _).trans (natDegree_map_le f p)