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.map (↑f) (roots p) ≤ 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.map (↑f) (roots p) ≤ 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.map (↑f) (roots p) ≤ 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.map (↑f) (roots p) ≤ roots (map f p)
exact map_roots_le ((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.map (↑f) (roots p) ≤ roots (map f p)
simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_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