Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-04 07:42 c10d1b1f

View on Github →

feat(ring_theory/polynomial/cyclotomic): add order_of_root_cyclotomic (#5151) Two lemmas about roots of cyclotomic polynomials modulo p. order_of_root_cyclotomic is the main algebraic tool to prove the existence of infinitely many primes congruent to 1 modulo n.

Estimated changes