X_pow_sub_C_irreducible_iff_of_prime_pow

English

Let p be prime. Then X^(p^n) − C a is irreducible if and only if for all d with d^p dividing p^n, and all b ∈ K, b^p ≠ a.

Русский

Пусть p — простое. Тогда X^(p^n) − C a ирредуцируемо тогда и только тогда, когда для всех d, удовлетворяющих выражению, и для всех b, b^p ≠ a.

LaTeX

$$$\\text{Irreducible}(X^{p^n} - C a) \\iff (\\forall d, d|p^n \\to d \\ne 1 \\to \\forall b, b^p \\ne a).$$$

Lean4

theorem X_pow_sub_C_irreducible_iff_of_prime_pow {p : ℕ} (hp : p.Prime) (hp' : p ≠ 2) {n} (hn : n ≠ 0) {a : K} :
    Irreducible (X ^ p ^ n - C a) ↔ ∀ b, b ^ p ≠ a :=
  ⟨(pow_ne_of_irreducible_X_pow_sub_C · (dvd_pow dvd_rfl hn) hp.ne_one), X_pow_sub_C_irreducible_of_prime_pow hp hp' n⟩

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