minpoly_dvd_cyclotomic — Mathlib

English

If n ≠ m, then cyclotomic(n, ℚ) and cyclotomic(m, ℚ) are coprime polynomials.

Русский

Если n ≠ m, то cyclotomic(n, ℚ) и cyclotomic(m, ℚ) взаимно простые полиномы.

LaTeX

$$$$ \\text{IsCoprime}(\\operatorname{cyclotomic}(n, \\mathbb{Q}), \\operatorname{cyclotomic}(m, \\mathbb{Q})). $$$$

Lean4

/-- The minimal polynomial of a primitive `n`-th root of unity `μ` divides `cyclotomic n ℤ`. -/
theorem _root_.IsPrimitiveRoot.minpoly_dvd_cyclotomic {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n)
    (hpos : 0 < n) [CharZero K] : minpoly ℤ μ ∣ cyclotomic n ℤ :=
  by
  apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)
  simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos

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