R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
ι : Type ?u.646647
h : 0 ≠ 1
p : R[X]
hp : Monic p
inst✝ : Nontrivial R
⊢ p ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.646647
h : 0 ≠ 1
p : R[X]
hp : Monic p
⊢ p ≠ 0
nontriviality R
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
ι : Type ?u.646647
h : 0 ≠ 1
p : R[X]
hp : Monic p
inst✝ : Nontrivial R
⊢ p ≠ 0
exact hp.ne_zero