R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : 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 : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
⊢ False
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : 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 : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
rw [A, eval₂_C] at hz
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = 0
⊢ False
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = 0
⊢ False
exact hp A