case pos
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
hp0 : p = 0
⊢ ↑Multiset.card (roots p) ≤ ↑Multiset.card (roots (map f p))

case neg
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
hp0 : ¬p = 0
⊢ ↑Multiset.card (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
hf : Function.Injective ↑f
⊢ ↑Multiset.card (roots p) ≤ ↑Multiset.card (roots (map f p))
by_cases hp0 : p = 0
no goals
case neg
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
hp0 : ¬p = 0
⊢ ↑Multiset.card (roots p) ≤ ↑Multiset.card (roots (map f p))
exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)
case pos
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
hp0 : p = 0
⊢ 0 ≤ 0
case pos
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
hp0 : p = 0
⊢ ↑Multiset.card (roots p) ≤ ↑Multiset.card (roots (map f p))
simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero]
no goals
case pos
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
hp0 : p = 0
⊢ 0 ≤ 0
rfl