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 = 1
this : coeff p 1 ≠ 0
⊢ IsRoot p (-(coeff p 0 / coeff p 1))
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 = 1
⊢ IsRoot p (-(coeff p 0 / coeff p 1))
have : p.coeff 1 ≠ 0 := by
  have h' := natDegree_eq_of_degree_eq_some h
  change natDegree p = 1 at h'; rw [←h']
  exact mt leadingCoeff_eq_zero.1 fun h0 => by simp [h0] 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 = 1
this : coeff p 1 ≠ 0
⊢ IsRoot (↑C (coeff p 1) * X + ↑C (coeff p 0)) (-(coeff p 0 / coeff p 1))
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 = 1
this : coeff p 1 ≠ 0
⊢ IsRoot p (-(coeff p 0 / coeff p 1))
conv in p => rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [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 p = 1
this : coeff p 1 ≠ 0
⊢ IsRoot (↑C (coeff p 1) * X + ↑C (coeff p 0)) (-(coeff p 0 / coeff p 1))
simp [IsRoot, mul_div_cancel' _ this]
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 = 1
h' : natDegree p = One.one
⊢ coeff p 1 ≠ 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 = 1
⊢ coeff p 1 ≠ 0
have h' := natDegree_eq_of_degree_eq_some 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 = 1
h' : natDegree p = 1
⊢ coeff p 1 ≠ 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 = 1
h' : natDegree p = One.one
⊢ coeff p 1 ≠ 0
change natDegree p = 1 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 = 1
h' : natDegree p = 1
⊢ coeff p (natDegree 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 = 1
h' : natDegree p = 1
⊢ coeff p 1 ≠ 0
rw [←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 p = 1
h' : natDegree p = 1
⊢ coeff p (natDegree p) ≠ 0
exact mt leadingCoeff_eq_zero.1 fun h0 => by simp [h0] 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 p = 1
h' : natDegree p = 1
h0 : p = 0
⊢ False
simp [h0] 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 p = 1
this : coeff p 1 ≠ 0
⊢ degree p ≤ 1
rw [h]