English
If n is such that n in R equals 0 and b is a unit, then the polynomial a C X^n + b X + c is separable.
Русский
Если элемент n в R равен нулю и b — единица, то многочлен a C X^n + b X + c сепарабелен.
LaTeX
$$$ (C a \cdot X^n + C b \cdot X + C c) \Separable$ under the given constraint$$
Lean4
/-- If `n = 0` in `R` and `b` is a unit, then `a * X ^ n + b * X + c` is separable. -/
theorem separable_C_mul_X_pow_add_C_mul_X_add_C {n : ℕ} (a b c : R) (hn : (n : R) = 0) (hb : IsUnit b) :
(C a * X ^ n + C b * X + C c).Separable :=
by
set f := C a * X ^ n + C b * X + C c
obtain ⟨e, hb⟩ := hb.exists_left_inv
refine ⟨-derivative f, f + C e, ?_⟩
have hderiv : derivative f = C b := by simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]
rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add, ← map_mul, hb, map_one]
