R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
x : R
H : x = 0
⊢ ¬Irreducible 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
x : R
H : x = 0
⊢ ¬Irreducible (↑C x)
rw [H, C_0]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
x : R
H : x = 0
⊢ ¬Irreducible 0
exact not_irreducible_zero