English
For any natural number n, the separable degree of f^n equals 0 if n = 0, and equals natSepDegree(f) otherwise.
Русский
Для любого натурального числа n разделяемая степень f^n равна 0, если n = 0, и равна natSepDegree(f) в противном случае.
LaTeX
$$$ (f^n).\operatorname{natSepDegree} = \begin{cases} 0, & n=0 \\ \operatorname{natSepDegree}(f), & n\neq 0 \end{cases}$$$
Lean4
@[simp]
theorem natSepDegree_pow {n : ℕ} : (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree := by
classical
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]
by_cases h : n = 0
· simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]
simp only [h, Multiset.toFinset_nsmul _ n h, ite_false]
