Commit 2020-12-21 15:29 96a2aa1d

feat(ring_theory/roots_of_unity): add minimal_polynomial_eq_pow (#5444) This is the main result about minimal polynomial of primitive roots of unity: μ and μ ^ p have the same minimal polynomial. The proof is a little long, but I don't see how I can split it: it is entirely by contradiction, so any lemma extracted from it would start with a false assumption and at the end it would be used only in this proof.