English
There exists a unique polynomial P ∈ ℤ[X] such that map (Int.castRingHom K) P = cyclotomic' n K.
Русский
Существует единственный полином P ∈ ℤ[X], такой что map(Int.castRingHom K) P = cyclotomic' n K.
LaTeX
$$$\exists! P \in \mathbb{Z}[X],\ map(\operatorname{Int.castRingHom}K)P = \operatorname{cyclotomic}'(n,K)$$$
Lean4
/-- If `K` is of characteristic `0` and there is a primitive `n`-th root of unity in `K`,
then `cyclotomic n K` comes from a unique polynomial with integer coefficients. -/
theorem unique_int_coeff_of_cycl {K : Type*} [CommRing K] [IsDomain K] [CharZero K] {ζ : K} {n : ℕ+}
(h : IsPrimitiveRoot ζ n) : ∃! P : ℤ[X], map (Int.castRingHom K) P = cyclotomic' n K :=
by
obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h
refine ⟨P, hP.1, fun Q hQ => ?_⟩
apply map_injective (Int.castRingHom K) Int.cast_injective
rw [hP.1, hQ]
