R✝ : Type u
S : Type v
a b c d : R✝
n m : ℕ
inst✝² : Semiring R✝
p q : R✝[X]
ι : Type ?u.645873
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False
R✝ : Type u
S : Type v
a b c d : R✝
n m : ℕ
inst✝² : Semiring R✝
p✝ q : R✝[X]
ι : Type ?u.645873
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : Monic p
⊢ p ≠ 0
rintro rfl
no goals
R✝ : Type u
S : Type v
a b c d : R✝
n m : ℕ
inst✝² : Semiring R✝
p q : R✝[X]
ι : Type ?u.645873
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False
simp [Monic] at hp