English
Over ℂ, the image of cyclotomic n ℤ under the complex embedding equals cyclotomic' n ℂ; their degrees agree and cyclotomic n ℤ is monic.
Русский
Над парой полей ℂ полное отображение циклотоми́ческого n ℤ совпадает с cyclotomic' n ℂ; степени равны, и cyclotomic n ℤ моноичен.
LaTeX
$$$\operatorname{map}(\operatorname{Int.castRingHom}\mathbb{C})\big(\operatorname{cyclotomic}(n,\mathbb{Z})\big) = \operatorname{cyclotomic}'(n,\mathbb{C}) \land \\ (\operatorname{cyclotomic}(n,\mathbb{Z})).\deg = (\operatorname{cyclotomic}'(n,\mathbb{C})).\deg \land (\operatorname{cyclotomic}(n,\mathbb{Z})).Monic$$
Lean4
theorem int_cyclotomic_spec (n : ℕ) :
map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
(cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic :=
by
by_cases hzero : n = 0
· simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos, Polynomial.map_one, and_self_iff]
rw [int_cyclotomic_rw hzero]
exact (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec
