R : Type u
inst✝ : CommRing R
f g : R[X]
hf : Separable f
hg : Separable g
h : IsCoprime f g
⊢ IsCoprime (f * g) (↑derivative f * g + f * ↑derivative g)
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : Separable f
hg : Separable g
h : IsCoprime f g
⊢ Separable (f * g)
rw [separable_def, derivative_mul]
no goals
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : Separable f
hg : Separable g
h : IsCoprime f g
⊢ IsCoprime (f * g) (↑derivative f * g + f * ↑derivative g)
exact
  ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)