English
The cyclotomic' for n equals the quotient of X^n - 1 by the product over the proper divisors of n of cyclotomic' i K.
Русский
cyclotomic'(n,K) = (X^n - 1) / ∏_{i ∈ properDivisors(n)} cyclotomic'(i,K).
LaTeX
$$$\operatorname{cyclotomic}'(n,K) = \dfrac{X^n - 1}{\prod_{i \in \operatorname{properDivisors}(n)} \operatorname{cyclotomic}'(i,K)}$$$
Lean4
/-- If there is a primitive `n`-th root of unity in `K`, then
`cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic' i K)`. -/
theorem cyclotomic'_eq_X_pow_sub_one_div {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n)
(h : IsPrimitiveRoot ζ n) : cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i ∈ Nat.properDivisors n, cyclotomic' i K :=
by
rw [← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
have prod_monic : (∏ i ∈ Nat.properDivisors n, cyclotomic' i K).Monic :=
by
apply monic_prod_of_monic
intro i _
exact cyclotomic'.monic i K
rw [(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1]
simp only [degree_zero, zero_add]
refine ⟨by rw [mul_comm], ?_⟩
rw [bot_lt_iff_ne_bot]
intro h
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
