feat(*): assorted prereqs for cyclotomic polynomials (#4887)
This is hopefully my last preparatory PR for cyclotomic polynomials. It was in [4869](https://github.com/leanprover-community/mathlib/pull/4869) .
Co-authored-by: Johan Commelin <johan@commelin.net>
