mathlib

b7024088 - feat(ring_theory/roots_of_unity): add squarefreeness mod p of minimal polynomial (#5381)

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.