English
If an expanded polynomial is separable, then either the base polynomial is a unit or the expansion parameter n is zero; otherwise, the base polynomial must be a unit or zero.
Русский
Если расширение полиомиального вида, полученное через разложение, сепарабельно, то либо исходный многочлен является единицей, либо n равно нулю; иначе исходный многочлен единица или ноль.
LaTeX
$$$f\\;\\text{Separable} \\Rightarrow (\\text{IsUnit}(f) \\lor n=0)$$$
Lean4
theorem isUnit_or_eq_zero_of_separable_expand {f : F[X]} (n : ℕ) (hp : 0 < p) (hf : (expand F (p ^ n) f).Separable) :
IsUnit f ∨ n = 0 := by
rw [or_iff_not_imp_right]
rintro hn : n ≠ 0
have hf2 : derivative (expand F (p ^ n) f) = 0 := by
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
rcases hf with ⟨r, hr, hrf⟩
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
rwa [hrf, isUnit_C]
