R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
⊢ ¬IsField R[X]
R : Type u
S : Type ?u.190529
inst✝ : Ring R
⊢ ¬IsField R[X]
nontriviality R
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
⊢ False
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
⊢ ¬IsField R[X]
intro hR
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
⊢ False
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
⊢ False
obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
⊢ False
have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : degree p < degree (p * X)
⊢ False
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False
have := degree_lt_degree_mul_X hp0
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : degree p < degree (p * X)
⊢ False
rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this
no goals
case intro
R : Type u
S : Type ?u.190529
inst✝ : Ring R
✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False
exact hp0 this