int_cyclotomic_unique — Mathlib

English

If a polynomial P ∈ ℤ[X] maps to cyclotomic' n ℂ under the complex embedding, then P equals cyclotomic n ℤ.

Русский

Если P ∈ ℤ[X] отображается как cyclotomic' n ℂ, то P равно cyclotomic n ℤ.

LaTeX

$$$\forall P \in \mathbb{Z}[X],\ map(\operatorname{Int.castRingHom}\mathbb{C})P = \operatorname{cyclotomic}'(n,\mathbb{C}) \Rightarrow P = \operatorname{cyclotomic}(n,\mathbb{Z})$$$

Lean4

theorem int_cyclotomic_unique {n : ℕ} {P : ℤ[X]} (h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ) :
    P = cyclotomic n ℤ := by
  apply map_injective (Int.castRingHom ℂ) Int.cast_injective
  rw [h, (int_cyclotomic_spec n).1]

Похожие утверждения