Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 15:19 fb9c5d30

View on Github →

feat(cyclotomic/basic): diverse roots of unity lemmas (#11473) From flt-regular.

Estimated changes

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

added theorem polynomial.cyclotomic.roots_eq_primitive_roots_val

added theorem polynomial.cyclotomic.roots_to_finset_eq_primitive_roots

modified theorem polynomial.is_root_cyclotomic

modified theorem polynomial.is_root_cyclotomic_iff

added theorem polynomial.is_root_of_unity_of_root_cyclotomic

added theorem polynomial.roots_cyclotomic_nodup