R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
⊢ degree p = 1
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
⊢ degree p = 1
have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
h₂ : degree (X - ↑C x) = 0
⊢ degree p = 1
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
⊢ degree p = 1
have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
h₂ : 1 = 0
⊢ degree p = 1
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
h₂ : degree (X - ↑C x) = 0
⊢ degree p = 1
rw [h₁] at h₂
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
h₂ : 1 = 0
⊢ degree p = 1
exact absurd h₂ (by decide)
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
h : IsUnit (X - ↑C x)
h₁ : degree (X - ↑C x) = 1
h₂ : 1 = 0
⊢ ¬1 = 0
decide
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hi : Irreducible p
x : R
hx : IsRoot p x
g : R[X]
hg : p = (X - ↑C x) * g
this : IsUnit (X - ↑C x) ∨ IsUnit g
hgu : IsUnit g
⊢ degree p = 1
rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]