Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 8, 2022

This PR will likely be subsumed by defining and using Laurent polynomials: the coefficients of a Laurent polynomial are naturally indexed by an integer.

ℤ-coefficients of polynomials

Let R be a (semi)ring, let f : R[X] be a polynomial and let n : ℤ be an integer.

This file defines f.zcoeff n : R, the coefficient of a polynomial in degree n : ℤ,
where we assign coefficient 0 to every negative degree. Thus, p.zcoeff n coincides with
p.coeff n, when 0 ≤ n and equals 0 otherwise.

Zulip


Open in Gitpod

@adomani adomani added RFC Request for comment awaiting-author A reviewer has asked the author a question or requested changes labels Apr 8, 2022
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes RFC Request for comment too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants