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
h : map f p ≠ 0
⊢ ↑Multiset.card (Multiset.map (↑f) (roots p)) ≤ ↑Multiset.card (roots (map f 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
h : map f p ≠ 0
⊢ ↑Multiset.card (roots p) ≤ ↑Multiset.card (roots (map f p))
rw [← p.roots.card_map f]
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
h : map f p ≠ 0
⊢ ↑Multiset.card (Multiset.map (↑f) (roots p)) ≤ ↑Multiset.card (roots (map f p))
exact Multiset.card_le_of_le (map_roots_le h)