roots_cyclotomic_nodup — Mathlib

English

For a domain R and NeZero(n in R), the roots of cyclotomic n R form a nodal (no repetition) set.

Русский

Для области R и ненулного n в R корни cyclotomic n R образуют безповторный набор.

LaTeX

$$$$ (\\operatorname{cyclotomic}(n, R)).\\text{roots}.\\text{Nodup}. $$$$

Lean4

theorem roots_cyclotomic_nodup [NeZero (n : R)] : (cyclotomic n R).roots.Nodup :=
  by
  obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
  · exact h.symm ▸ Multiset.nodup_zero
  rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ
  refine
    Multiset.nodup_of_le
      (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <| cyclotomic.dvd_X_pow_sub_one n R)
      hζ.nthRoots_one_nodup

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