separable_X_pow_sub_C — Mathlib

English

If n ≠ 0 and a ≠ 0 in F, then X^n − a is separable over F.

Русский

Если n ≠ 0 и a ≠ 0 в F, то X^n − a сепарабельен над F.

LaTeX

$$$\\text{Separable}(X^n - C a)$ for $n \\neq 0$ and $a \neq 0$.$$

Lean4

/-- If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`. -/
theorem separable_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) : Separable (X ^ n - C a) :=
  separable_X_pow_sub_C_unit (Units.mk0 a ha) (IsUnit.mk0 (n : F) hn)

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