Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-03 15:26 83f40364

View on Github →

feat(*/cyclotomic): update is_root_cyclotomic_iff to use ne_zero (#11071)

Estimated changes

Modified src/number_theory/primes_congruent_one.lean

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

modified theorem polynomial.is_root_cyclotomic_iff

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