R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R[X]
n : ℕ
h : Separable (f * (f * f ^ n))
⊢ IsUnit f ∨ Separable f ∧ n + 2 = 1 ∨ n + 2 = 0
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R[X]
n : ℕ
h : Separable (f ^ (n + 2))
⊢ IsUnit f ∨ Separable f ∧ n + 2 = 1 ∨ n + 2 = 0
rw [pow_succ, pow_succ] at h
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R[X]
n : ℕ
h : Separable (f * (f * f ^ n))
⊢ IsUnit f ∨ Separable f ∧ n + 2 = 1 ∨ n + 2 = 0
exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_right_left)