English
As above for a commutative domain R where X^n − C a factors via a primitive root of unity, giving the explicit product expansion.
Русский
Как выше для коммутативного домена R, где X^n − C a раскладывается через примитивный корень единицы, приводя явное разложение на произведение.
LaTeX
$$$X^n - C a = \\prod_{i=0}^{n-1} (X - C(\\zeta^i \\alpha)).$$$
Lean4
theorem X_pow_sub_C_eq_prod {R : Type*} [CommRing R] [IsDomain R] {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α a : R}
(hn : 0 < n) (e : α ^ n = a) : (X ^ n - C a) = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)) :=
by
let K := FractionRing R
let i := algebraMap R K
have h := FaithfulSMul.algebraMap_injective R K
apply_fun Polynomial.map i using map_injective i h
simpa only [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, map_mul, map_pow, Polynomial.map_prod,
Polynomial.map_mul] using X_pow_sub_C_eq_prod' (hζ.map_of_injective h) hn <| map_pow i α n ▸ congrArg i e
