X_pow_sub_C_irreducible_iff_of_odd

English

Let n be odd. X^n − C a is irreducible over K if and only if, for every d dividing n with d ≠ 1, and for all b ∈ K, b^d ≠ a.

Русский

Пусть n нечётно. X^n − C a ирредуцируемо над K тогда и только тогда, когда для каждого d|n с d ≠ 1 и для всех b ∈ K верно b^d ≠ a.

LaTeX

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

Lean4

theorem X_pow_sub_C_irreducible_iff_of_odd {n : ℕ} (hn : Odd n) {a : K} :
    Irreducible (X ^ n - C a) ↔ (∀ d, d ∣ n → d ≠ 1 → ∀ b : K, b ^ d ≠ a) :=
  ⟨fun e _ ↦ pow_ne_of_irreducible_X_pow_sub_C e, fun H ↦
    X_pow_sub_C_irreducible_of_odd hn fun p hp hpn ↦ (H p hpn hp.ne_one)⟩
    -- TODO: generalize to `p = 2`

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