no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree p = 0
⊢ degree p ≤ 0
simp [*, le_refl]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree (↑C 0) = 0
this : degree p ≤ 0
hc : coeff p 0 = 0
⊢ False
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree p = 0
this : degree p ≤ 0
hc : coeff p 0 = 0
⊢ False
rw [eq_C_of_degree_le_zero this, hc] at h
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree (↑C 0) = 0
this : degree p ≤ 0
hc : coeff p 0 = 0
⊢ False
simp at h
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree p = 0
this : degree p ≤ 0
hc : coeff p 0 ≠ 0
⊢ 1 = ↑C (coeff p 0) * ↑C (coeff p 0)⁻¹
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree p = 0
this : degree p ≤ 0
hc : coeff p 0 ≠ 0
⊢ 1 = p * ↑C (coeff p 0)⁻¹
conv in p => rw [eq_C_of_degree_le_zero this]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
h : degree p = 0
this : degree p ≤ 0
hc : coeff p 0 ≠ 0
⊢ 1 = ↑C (coeff p 0) * ↑C (coeff p 0)⁻¹
rw [← C_mul, _root_.mul_inv_cancel hc, C_1]