case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
g f' : R[X]
hf : Separable (g * f')
⊢ Separable g
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
hf : Separable f
hfg : g ∣ f
⊢ Separable g
rcases hfg with ⟨f', rfl⟩
no goals
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
g f' : R[X]
hf : Separable (g * f')
⊢ Separable g
exact Separable.of_mul_left hf