feat(data/polynomial/mirror): new file (#6426)
This files defines an alternate version of `polynomial.reverse`. This version is often nicer to work with since it preserves `nat_degree` and `nat_trailing_degree` and is always an involution.
(this PR is part of the irreducibility saga)
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
