mathlib

d74046a6 - feat(data/polynomial): monic.as_sum

feat(data/polynomial): monic.as_sum From the perfectoid project. It is often useful to write a monic polynomial f in the form `X^n + sum of lower degree terms`.