cyclotomic_eq_minpoly_rat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `cyclotomic n ℚ` is the minimal polynomial of a primitive `n`-th root of unity `μ`. -/
theorem cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n)
    [CharZero K] : cyclotomic n ℚ = minpoly ℚ μ :=
  by
  rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]
  exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm

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