English
If X^n − C a is irreducible, then no nontrivial m dividing n yields b^m = a for any b ∈ K when m ≠ 1.
Русский
Если X^n − C a иррeд, то никакое m|n с m ≠ 1 не даёт существование b ∈ K с b^m = a.
LaTeX
$$$\forall m|n, m\neq 1:\forall b\in K:\, b^m \neq a$$$
Lean4
theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n)
(hm' : m ≠ 1) (b : K) : b ^ m ≠ a :=
by
have hn : n ≠ 0 := fun e ↦ not_irreducible_C (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
obtain ⟨k, rfl⟩ := hm
rintro rfl
obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
rw [mul_comm, pow_mul, map_pow, hq] at H
have : degree q = 0 := by
simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C, Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 rfl
apply_fun degree at hq
simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero, Nat.cast_injective.eq_iff] at hq
exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)
