R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
p : R[X]
hp : IsPrimitive p
⊢ p ≠ 0
rintro rfl
no goals
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False
exact (hp 0 (dvd_zero (C 0))).ne_zero rfl