mathlib3

96a2aa1d - feat(ring_theory/roots_of_unity): add minimal_polynomial_eq_pow (#5444)

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. Co-authored-by: Johan Commelin <johan@commelin.net>