mathlib

5eb68b5c - feat(data/polynomial/mirror): `nat_degree` and `nat_trailing_degree` of `p * p.mirror` (#14397)

feat(data/polynomial/mirror): `nat_degree` and `nat_trailing_degree` of `p * p.mirror` (#14397) This PR adds lemmas for the `nat_degree` and `nat_trailing_degree` of `p * p.mirror`. These lemmas tell you that you can recover `p.nat_degree` and `p.nat_trailing_degree` from `p * p.mirror`, which will be useful for irreducibility of x^n-x-1.