mathlib

82ec0ccb - feat(ring_theory/roots_of_unity): degree of minimal polynomial (#5475)

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 `n`th 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`.