isRoot_cyclotomic_iff_charZero — Mathlib

English

Over a characteristic zero domain, a cyclotomic polynomial cyclotomic(n, R) has a root μ if and only if μ is a primitive n-th root of unity.

Русский

В области характеристика ноль полином cyclotomic(n, R) имеет корень μ тогда и только тогда, когда μ является примитивным n-ым корнем единицы.

LaTeX

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

Lean4

/-- If `R` is of characteristic zero, then `ζ` is a root of `cyclotomic n R` if and only if it is a
primitive `n`-th root of unity. -/
theorem isRoot_cyclotomic_iff_charZero {n : ℕ} {R : Type*} [CommRing R] [IsDomain R] [CharZero R] {μ : R} (hn : 0 < n) :
    (Polynomial.cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n :=
  letI := NeZero.of_gt hn
  isRoot_cyclotomic_iff

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