English
For any polynomial f, for any n, if (f^n) is separable, then either f is a unit, or f is separable and n = 1 or n = 0.
Русский
Для любого многочлена f и любого n: если f^n разделим, то либо f — единица, либо f разделим и n = 1, либо n = 0.
LaTeX
$$$\\forall n:\\n (f^n)\\Separable \\Rightarrow (\\operatorname{IsUnit}(f) \\lor (f\\Separable \\land n = 1) \\lor n = 0)$$$
Lean4
theorem of_pow' {f : R[X]} : ∀ {n : ℕ} (_h : (f ^ n).Separable), IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
| 0 => fun _h => Or.inr <| Or.inr rfl
| 1 => fun h => Or.inr <| Or.inl ⟨pow_one f ▸ h, rfl⟩
| n + 2 => fun h => by
rw [pow_succ, pow_succ] at h
exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)
