R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative (f * g))
⊢ Separable f
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
⊢ Separable f
have := h.of_mul_left_left
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative f * g + f * ↑derivative g)
⊢ Separable f
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative (f * g))
⊢ Separable f
rw [derivative_mul] at this
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative f * g + f * ↑derivative g)
⊢ Separable f
exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)