English
For any n and unit u in R, the polynomial X^n − u is separable.
Русский
Для любого n и единицы u равной в кольце R множитель X^n − u сепарабелен.
LaTeX
$$$ \operatorname{Separable}\left( X^n - C(u) \right)$$$
Lean4
/-- If `IsUnit n` in a `CommRing R`, then `X ^ n - u` is separable for any unit `u`. -/
theorem separable_X_pow_sub_C_unit {n : ℕ} (u : Rˣ) (hn : IsUnit (n : R)) : Separable (X ^ n - C (u : R)) :=
by
nontriviality R
rcases n.eq_zero_or_pos with (rfl | hpos)
· simp at hn
apply (separable_def' (X ^ n - C (u : R))).2
obtain ⟨n', hn'⟩ := hn.exists_left_inv
refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
calc
-C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) :=
by
simp only [C.map_mul, C_eq_natCast]
ring
_ = 1 := by
simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ', Nat.sub_add_cancel (show 1 ≤ n from hpos),
sub_add_cancel]
