cyclotomic_eq_minpoly — Mathlib

English

The cyclotomic ℤ polynomial is the minimal polynomial of a primitive nth root of unity μ.

Русский

Циклотоми́ческий полином ℤ является минимальным полиномом примитивного μ n-ого корня единницы.

LaTeX

$$$$ \\operatorname{cyclotomic}(n, \\mathbb{Z}) = \\minpoly_{\\mathbb{Z}}(\\mu) $$$$

Lean4

/-- `cyclotomic n ℤ` is the minimal polynomial of a primitive `n`-th root of unity `μ`. -/
theorem cyclotomic_eq_minpoly {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n)
    [CharZero K] : cyclotomic n ℤ = minpoly ℤ μ :=
  by
  refine
    eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos)) (cyclotomic.monic n ℤ)
      (h.minpoly_dvd_cyclotomic hpos) ?_
  simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h

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