R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
a : R
⊢ IsCoprime (X + ↑C a) 1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
a : R
⊢ Separable (X + ↑C a)
rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
a : R
⊢ IsCoprime (X + ↑C a) 1
exact isCoprime_one_right