R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
⊢ IsCoprime X 1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
⊢ Separable X
rw [separable_def, derivative_X]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
⊢ IsCoprime X 1
exact isCoprime_one_right