Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 06:35 8915dc8e

View on Github →

feat(ring_theory/polynomial/cyclotomic): is_root_cyclotomic_iff (#10422) From the flt-regular project.

Estimated changes

Modified src/number_theory/primes_congruent_one.lean

Modified src/ring_theory/polynomial/cyclotomic.lean

added theorem is_root_of_unity_iff

added theorem polynomial.is_root_cyclotomic_iff

deleted theorem polynomial.order_of_root_cyclotomic_eq