Commit 2020-12-15 21:09 b7024088
View on Github →feat(ring_theory/roots_of_unity): add squarefreeness mod p of minimal polynomial (#5381)
Two easy results about the reduction mod p of the minimal polynomial over ℤ of a primitive root of unity: it is separable and hence squarefree.