-
Notifications
You must be signed in to change notification settings - Fork 299
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
[Merged by Bors] - feat(data/mv_polynomial/equiv): API for mv_polynomial.fin_succ_equiv
#10812
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some style comments
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry for forgetting about this PR. I've been too busy with non-lean things lately.
bors merge
#10812) This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...): |
#10812) This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...): |
#10812) This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed: |
Please merge |
✌️ isadofschi can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
#10812) This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
mv_polynomial.fin_succ_equiv
mv_polynomial.fin_succ_equiv
This PR provides API for
mv_polynomial.fin_succ_equiv
: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc.To state and prove these lemmas I had to define
cons
andtail
for mapsfin (n+1) →₀ M
and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this.