mathlib3
866be5f6 - feat(data/polynomial): monic.as_sum (#1773)

Commit

6 years ago

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

References

#1773 - feat(data/polynomial): monic.as_sum

Author

jcommelin

Committer

mergify[bot]

Parents

922a4ebe

mathlib3 866be5f6 - feat(data/polynomial): monic.as_sum (#1773)

mathlib3
866be5f6 - feat(data/polynomial): monic.as_sum (#1773)