roots_of_cyclotomic — Mathlib

English

The roots of cyclotomic' n R are exactly the primitive n-th roots of unity in R.

Русский

Корни cyclotomic' n R совпадают ровно с примитивными n-ми корнями единицы в R.

LaTeX

$$$\operatorname{roots}(\operatorname{cyclotomic}'(n,R)) = (\operatorname{primitiveRoots}(n,R)).\text{val}$$$

Lean4

/-- The roots of `cyclotomic' n R` are the primitive `n`-th roots of unity. -/
theorem roots_of_cyclotomic (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] :
    (cyclotomic' n R).roots = (primitiveRoots n R).val := by rw [cyclotomic'];
  exact roots_prod_X_sub_C (primitiveRoots n R)

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