mathlib

9f6f605b - feat(data/polynomial/mirror): Central coefficient of `p * p.mirror` (#14096)

feat(data/polynomial/mirror): Central coefficient of `p * p.mirror` (#14096) This PR adds a lemma `(p * p.mirror).coeff (p.nat_degree + p.nat_trailing_degree) = p.sum (λ n, (^ 2))`. I also rearranged the file by assumptions on the ring `R`.