Commit 2020-12-19 17:55 ce385a05

feat(ring_theory/roots_of_unity): lemmas about minimal polynomial (#5393) Three results about the minimal polynomial of μ and μ ^ p, where μ is a primitive root of unity. These are preparatory lemmas to prove that the two minimal polynomials are equal.