isRoot_cyclotomic — Mathlib

English

Any n-th primitive root μ is a root of the cyclotomic polynomial cyclotomic n R.

Русский

Любой примитивный корень n-ой степени μ является корнем полинома cyclotomic n R.

LaTeX

$$$$ \\text{IsRoot}(\\operatorname{cyclotomic}(n, R), \\mu). $$$$

Lean4

/-- Any `n`-th primitive root of unity is a root of `cyclotomic n R`. -/
theorem _root_.IsPrimitiveRoot.isRoot_cyclotomic (hpos : 0 < n) {μ : R} (h : IsPrimitiveRoot μ n) :
    IsRoot (cyclotomic n R) μ :=
  by
  rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h, roots_prod_X_sub_C, ←
    Finset.mem_def]
  rwa [← mem_primitiveRoots hpos] at h

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