roots_to_finset_eq_primitiveRoots

English

The finite set of roots of cyclotomic n R coincides with the multiset of primitive n-th roots of unity, viewed as a finite set.

Русский

Множество корней cyclotomic n R совпадает с множеством примитивных n-ных корней единницы, считанных как конечное множество.

LaTeX

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

Lean4

theorem roots_to_finset_eq_primitiveRoots [NeZero (n : R)] :
    (⟨(cyclotomic n R).roots, roots_cyclotomic_nodup⟩ : Finset _) = primitiveRoots n R :=
  by
  ext a
  simp [cyclotomic_ne_zero n R, ← isRoot_cyclotomic_iff, mem_primitiveRoots, NeZero.pos_of_neZero_natCast R]

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