Commit 2021-01-05 20:33 82ec0ccb

feat(ring_theory/roots_of_unity): degree of minimal polynomial (#5475) This is the penultimate PR about roots of unity and cyclotomic polynomials: I prove that the degree of the minimal polynomial of a primitive nth root of unity is at least nat.totient n. It's easy to prove now that it is actually nat.totient n, and indeed that the minimal polynomial is the cyclotomic polynomial (that it is hence irreducible). I decided to split the PR like this because I feel that it's better to put the remaining results in ring_theory/polynomials/cyclotomic.