roots_eq_primitiveRoots_val — Mathlib

English

The roots of cyclotomic n R are exactly the elements listed by the primitiveRoots set for n.

Русский

Корни cyclotomic n R совпадают с элементами множества primitiveRoots(n, R).

LaTeX

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

Lean4

theorem roots_eq_primitiveRoots_val [NeZero (n : R)] : (cyclotomic n R).roots = (primitiveRoots n R).val := by
  rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]

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