X_pow_sub_C_irreducible_of_prime_pow

English

For a prime p and n≥1 with p ≠ 2, X^(p^n) − C a is irreducible if and only if for all b, b^p ≠ a.

Русский

Для простого p, p ≠ 2, и n≥1: X^(p^n) − C a ирредуцируемо тогда и только тогда, когда для всех b: b^p ≠ a.

LaTeX

$$$\\text{Irreducible}(X^{p^n} - C a) \\iff (\\forall b, b^p \\neq a).$$$

Lean4

theorem X_pow_sub_C_irreducible_of_prime_pow {p : ℕ} (hp : p.Prime) (hp' : p ≠ 2) (n : ℕ) {a : K}
    (ha : ∀ b : K, b ^ p ≠ a) : Irreducible (X ^ (p ^ n) - C a) :=
  by
  apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow
  intro q hq hq'
  simpa [(Nat.prime_dvd_prime_iff_eq hq hp).mp (hq.dvd_of_dvd_pow hq')] using ha

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