English
If n is odd and for every p prime dividing n and every b in K, b^p ≠ a, then X^n − C a is irreducible over K.
Русский
Если n нечётно и для каждого простого p|n и каждого b ∈ K выполняется b^p ≠ a, то X^n − C a ирредуцируем над K.
LaTeX
$$$\\text{Irreducible}(X^n - C a)$ under the given hypothesis.$$
Lean4
theorem X_pow_sub_C_irreducible_of_odd {n : ℕ} (hn : Odd n) {a : K}
(ha : ∀ p : ℕ, p.Prime → p ∣ n → ∀ b : K, b ^ p ≠ a) : Irreducible (X ^ n - C a) := by
induction n using induction_on_primes generalizing K a with
| zero => simp [← Nat.not_even_iff_odd] at hn
| one => simpa using irreducible_X_sub_C a
| prime_mul p n hp IH =>
rw [mul_comm]
apply X_pow_mul_sub_C_irreducible (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))
intro E _ _ x hx
have : IsIntegral K x :=
not_not.mp fun h ↦ by
simpa only [degree_zero, degree_X_pow_sub_C hp.pos, WithBot.natCast_ne_bot] using
congr_arg degree (hx.symm.trans (dif_neg h))
apply IH (Nat.odd_mul.mp hn).2
intro q hq hqn b hb
apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)
rw [← map_pow, hb, ← adjoin.powerBasis_gen this, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]
simp [minpoly_gen, hx, hp.ne_zero.symm, (Nat.odd_mul.mp hn).1.neg_pow]
