minpoly_eq_cyclotomic_of_irreducible

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible {K : Type*} [Field K] {R : Type*} [CommRing R]
    [IsDomain R] {μ : R} {n : ℕ} [Algebra K R] (hμ : IsPrimitiveRoot μ n) (h : Irreducible <| cyclotomic n K)
    [NeZero (n : K)] : cyclotomic n K = minpoly K μ :=
  by
  haveI := NeZero.of_faithfulSMul K R n
  refine minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)
  rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]

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