feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| (#12595)
Originally from the Wedderburn PR, but generalized to include an exponent.
Co-authored-by: Alex J. Best <alex.j.best@gmail.com>
Co-authored-by: Alex J. Best <alex.j.best@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
