English
If ζ runs through all nth roots of unity, then X^n - 1 factors as the product of (X - ζ) over all nth roots of unity.
Русский
Если ζ пробегает по всем n-ым корням единицы, то X^n - 1 раскладывается как произведение (X - ζ) по всем n-ым корням единицы.
LaTeX
$$$X^n - 1 = \prod_{\zeta \in \operatorname{nthRootsFinset}(n,1)} (X - C\zeta)$$$
Lean4
/-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - 1 = ∏ (X - μ)`, where `μ`
varies over the `n`-th roots of unity. -/
theorem X_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n (1 : R), (X - C ζ) := by
classical
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]
simp only [Finset.prod_mk]
rw [nthRoots]
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
symm
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
exact IsPrimitiveRoot.card_nthRoots_one h
