mathlib

c10d1b1f - feat(ring_theory/polynomial/cyclotomic): add order_of_root_cyclotomic (#5151)

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`. Co-authored-by: Johan Commelin <johan@commelin.net>