R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
⊢ False
have := eq_C_of_degree_le_zero hlt
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
rw [IsRoot, this, eval_C] at h
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = 0
⊢ False
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
simp only [h, RingHom.map_zero] at this
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = 0
⊢ False
exact hp this