English
If there exists a primitive n-th root ζ in a ring K, then Φ_n K equals the product over primitive roots μ of (X − C μ). In particular, Φ_n K equals the cyclotomic' n K.
Русский
Если в кольце K существует примитивный корень n-й степени единицы ζ, то Φ_n K = ∏_{μ ∈ primitiveRoots n K} (X − C μ). В частности, Φ_n K = cyclotomic' n K.
LaTeX
$$$$\mathrm{cyclotomic}\ n\ K = \prod_{\mu \in \mathrm{primitiveRoots}\ n\ K} \bigl(X - C\mu\bigr).$$$$
Lean4
/-- If there is a primitive `n`-th root of unity in `K`, then
`cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ)`. ∈ particular,
`cyclotomic n K = cyclotomic' n K` -/
theorem cyclotomic_eq_prod_X_sub_primitiveRoots {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ}
(hz : IsPrimitiveRoot ζ n) : cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ) :=
by
rw [← cyclotomic']
induction n using Nat.strong_induction_on generalizing ζ with
| _ k hk
obtain hzero | hpos := k.eq_zero_or_pos
· simp only [hzero, cyclotomic'_zero, cyclotomic_zero]
have h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K :=
by
intro i hi
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
rw [mul_comm] at hd
exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)
rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz,
Finset.prod_congr (refl k.properDivisors) h]
