mathlib3

ce385a05 - feat(ring_theory/roots_of_unity): lemmas about minimal polynomial (#5393)

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.