R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (g * f)
⊢ Separable g
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
⊢ Separable g
rw [mul_comm] at h
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (g * f)
⊢ Separable g
exact h.of_mul_left