PR #13240: feat(data/polynomial/zcoeff): define zcoeff + API

Stream: triage

[Random Issue Bot]

Today I chose PR 13240 for discussion!

feat(data/polynomial/zcoeff): define zcoeff + API
Created by @damiano (@adomani) on 2022-04-08
Labels: RFC, awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

[Damiano Testa]

This PR will probably be closed, if/when enough degrees of add_monoid_algebras/laurent_polynomials will reach mathlib!