X_pow_sub_C_irreducible_iff_forall_prime_of_odd

English

For odd n, X^n − C a is irreducible over K if and only if for every prime p dividing n, b^p ≠ a for all b ∈ K.

Русский

Для нечётного n X^n − C a ирредуцируемый над K если и только если для каждого простого p|n для всех b∈K верно b^p ≠ a.

LaTeX

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

Lean4

theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd {n : ℕ} (hn : Odd n) {a : K} :
    Irreducible (X ^ n - C a) ↔ (∀ p : ℕ, p.Prime → p ∣ n → ∀ b : K, b ^ p ≠ a) :=
  ⟨fun e _ hp hpn ↦ pow_ne_of_irreducible_X_pow_sub_C e hpn hp.ne_one, X_pow_sub_C_irreducible_of_odd hn⟩

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