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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(data/polynomial): the d-1th coefficient of polynomial.map #7639

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(data/polynomial): the d-1th coefficient of polynomial.map #7639

wants to merge 1 commit into from

Conversation

Vierkantor
Copy link
Collaborator

We prove polynomial.next_coeff_map just like polynomial.leading_coeff_map'.

Open in Gitpod

@Vierkantor Vierkantor added the awaiting-review The author would like community review of the PR label May 17, 2021
@Vierkantor
feat(data/polynomial): the d-1th coefficient of polynomial.map
2672dc9 
We prove `polynomial.next_coeff_map` just like `polynomial.leading_coeff_map'`.
@Vierkantor Vierkantor mentioned this pull request May 17, 2021
Closed
8 tasks
@fpvandoorn
Copy link
Member

bors merge

Not related to this PR, but isn't polynomial.leading_coeff_map' strictly more general than polynomial.leading_coeff_map, and hence should replace it? Or am I missing something?

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 17, 2021
@Vierkantor
Copy link
Collaborator Author

leading_coeff_map' has an extra hypothesis hf : injective f, and leading_coeff_map has no explicit hypotheses (the injectivity follows from the field instances). So leading_coeff_map is a better simp lemma and leading_coeff_map' is more general. (Although we might want to golf the proof of leading_coeff_map to just leading_coeff_map' f.injective.)

bors bot pushed a commit that referenced this pull request May 17, 2021
@Vierkantor
feat(data/polynomial): the d-1th coefficient of polynomial.map (#…
b8a6995 
…7639)

We prove `polynomial.next_coeff_map` just like `polynomial.leading_coeff_map'`.
@bors
Copy link

bors bot commented May 18, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/polynomial): the d-1th coefficient of polynomial.map [Merged by Bors] - feat(data/polynomial): the d-1th coefficient of polynomial.map May 18, 2021
@bors bors bot closed this May 18, 2021
@bors bors bot deleted the next_coeff-map branch May 18, 2021 01:47
@fpvandoorn
Copy link
Member

Ah, that makes sense! I missed that extra hypothesis.

Vierkantor added a commit that referenced this pull request May 19, 2021
@Vierkantor
feat(data/polynomial): the d-1th coefficient of polynomial.map (#…
2faf664 
…7639)

We prove `polynomial.next_coeff_map` just like `polynomial.leading_coeff_map'`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@Vierkantor @fpvandoorn