ne_zero_of_irreducible_X_pow_sub_C

English

For prime p, if no b^p equals a, then X^p − C a is irreducible over K.

Русский

Для простого p, если ни одно b^p не даёт a, то X^p − C a ирродуцируемо над K.

LaTeX

$$$\text{If } p \text{ prime and } ∀ b\in K, b^p \neq a, \text{ then } X^p - C a \text{ is irreducible.}$$$

Lean4

theorem ne_zero_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) : n ≠ 0 :=
  by
  rintro rfl
  rw [pow_zero, ← C.map_one, ← map_sub] at H
  exact not_irreducible_C _ H

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