English
Let R be a commutative domain, and ζ a primitive n-th root of unity in R. If α^n = a in R with a ∈ R, then X^n − C a factors as a product ∏_{i=0}^{n-1} (X − C(ζ^i α)) in R[X].
Русский
Пусть R — коммутативный домен, ζ — примитивный корень единицы n-й степени в R. Пусть α^n = a в R. Тогда X^n − C a раскладывается как ∏_{i=0}^{n-1} (X − C(ζ^i α)) в R[X].
LaTeX
$$$X^n - C a = \\prod_{i=0}^{n-1} \\bigl(X - C(\\zeta^i \\alpha)\\bigr) \\quad \\text{in } R[X].$$$
Lean4
theorem X_pow_sub_C_splits_of_isPrimitiveRoot {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (e : α ^ n = a) :
(X ^ n - C a).Splits (RingHom.id _) := by
cases n.eq_zero_or_pos with
| inl hn =>
rw [hn, pow_zero, ← C.map_one, ← map_sub]
exact splits_C _ _
| inr hn =>
rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- make this private, as we only use it to prove a strictly more general version
