R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬IsField R[X]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
⊢ ¬IsField R[X]
nontriviality R
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ∃ I, ⊥ < I ∧ I < ⊤
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬IsField R[X]
rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ∃ I, ⊥ < I ∧ I < ⊤
use Ideal.span {Polynomial.X}
case left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X}

case right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ Ideal.span {X} < ⊤
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤
constructor
case left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬X = 0
case left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ⊥ < Ideal.span {X}
rw [bot_lt_iff_ne_bot, Ne.def, Ideal.span_singleton_eq_bot]
no goals
case left
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬X = 0
exact Polynomial.X_ne_zero
case right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬1 = 0
case right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ Ideal.span {X} < ⊤
rw [lt_top_iff_ne_top, Ne.def, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
  Polynomial.X_dvd_iff, Polynomial.coeff_one_zero]
no goals
case right
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
✝ : Nontrivial R
⊢ ¬1 = 0
exact one_ne_zero