separable_X_pow_sub_C' — Mathlib

English

Let F be a field of characteristic p. If p does not divide n and a ≠ 0 in F, then the polynomial X^n − a is separable over F.

Русский

Пусть F — поле характеристикe p. Если p не делит n и a ≠ 0 в F, то многочлен X^n − a над F разделим над F.

LaTeX

$$$(\\exists p \\; \\text{prime} \\; \\text{such that } \\operatorname{char}(F)=p) \\land p \\nmid n \\land a \\neq 0 \\Rightarrow \\text{Separable}(X^n - C a)$$$

Lean4

/-- If `F` is of characteristic `p` and `p ∤ n`, then `X ^ n - a` is separable for any `a ≠ 0`. -/
theorem separable_X_pow_sub_C' (p n : ℕ) (a : F) [CharP F p] (hn : ¬p ∣ n) (ha : a ≠ 0) : Separable (X ^ n - C a) :=
  separable_X_pow_sub_C a (by rwa [← CharP.cast_eq_zero_iff F p n] at hn) ha

Похожие утверждения