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/degree/basic): add lemmas dealing with monomials, their support and their nat_degrees #4475

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat(data/polynomial/degree/basic): add lemmas dealing with monomials, their support and their nat_degrees #4475

wants to merge 36 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Oct 6, 2020

adomani and others added 28 commits September 29, 2020 15:29
@adomani
begin induction
4ccabf2
@adomani
a dormire!
f4b243b
@adomani
mancano le disuguaglianze sugli esponenti
e552915
@adomani
induzione funziona!
1f59fdb
@adomani
Convertire il risultato vecchio
ffa0a6a
@adomani
cambio cases nell'induzione
f15752c
@adomani
formatting
e823610
@adomani
funiona!
d4e9a57
@adomani
before pushing
36026c5
@adomani
before pushing, saved pre_induction
ac82c8f
@adomani
Changes to be committed:
d06c2e9 
deleted:    induction.lean
deleted:    inductionv.lean
deleted:    mypol.lean
deleted:    pre_induction.lean
@adomani @awainverse
Update src/data/polynomial/degree/reverse_mul.lean
52ec9c5 
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
@adomani
Changed name of two lemmas
887e4b5
@adomani
Changes to be committed:
dd7caee 
deleted:    launch.json
@adomani
revised according to Aaron Anderson's comments.
8bac835 
**File still not split**
@adomani
Before changing namespace to erase_lead
ff92499
@adomani
Split!
d3fecec
@adomani
changed namespace from reverse to rev
dbbd75a
@adomani
min_max
6ef6097
@adomani
use image instead of ''
dc99797
@adomani
first version
6767b6c
@adomani
before clean-up
8f7d114
@adomani
updated following further comments from Aaron Anderson, cleaned up a …
e61a6e0 
…few proofs
@adomani
updated following comments from Aaron Anderson
2fccecc
@adomani
removed unchecked file
07031ed
@adomani
added a proof that the leading/trailing coefficient of the reflect of…
33911a8 
… f equal the traling/leading coefficient of f.
@adomani
merged lemmas into data/polynomial/degree/basic
136671c
@adomani
removed files of subsequent PRs
a3f7798
jcommelin
jcommelin reviewed Oct 6, 2020
View reviewed changes
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 6, 2020
adomani and others added 6 commits October 6, 2020 15:29
@adomani @jcommelin
Update src/data/polynomial/degree/basic.lean
1f197d4 
Co-authored-by: Johan Commelin <johan@commelin.net>
@adomani @jcommelin
Update src/data/polynomial/degree/basic.lean
4a0e45d 
Co-authored-by: Johan Commelin <johan@commelin.net>
@adomani @jcommelin
Update src/data/polynomial/degree/basic.lean
698e2ee 
Co-authored-by: Johan Commelin <johan@commelin.net>
@adomani @jcommelin
Update src/data/polynomial/degree/basic.lean
3ff1182 
Co-authored-by: Johan Commelin <johan@commelin.net>
@adomani
formatting change
69de31d
@adomani
Changes to be committed:
7bb3a7f 
modified:   basic.lean
@adomani adomani added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 6, 2020
jcommelin
jcommelin reviewed Oct 6, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One more comment

src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 6, 2020
jcommelin
jcommelin approved these changes Oct 6, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@jcommelin jcommelin added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 6, 2020
@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 Oct 6, 2020
@adomani
Copy link
Collaborator Author

adomani commented Oct 6, 2020

Thank you!

bors bot pushed a commit that referenced this pull request Oct 6, 2020
@adomani
feat(data/polynomial/degree/basic): add lemmas dealing with monomials…
5192fd9 
…, their support and their nat_degrees (#4475)
@bors
Copy link

bors bot commented Oct 6, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/polynomial/degree/basic): add lemmas dealing with monomials, their support and their nat_degrees [Merged by Bors] - feat(data/polynomial/degree/basic): add lemmas dealing with monomials, their support and their nat_degrees Oct 6, 2020
@bors bors bot closed this Oct 6, 2020
@bors bors bot deleted the rev_basic branch October 6, 2020 22:45
jcommelin pushed a commit that referenced this pull request Oct 7, 2020
@adomani @jcommelin
feat(data/polynomial/degree/basic): add lemmas dealing with monomials…
d41c321 
…, their support and their nat_degrees (#4475)
adomani added a commit that referenced this pull request Oct 7, 2020
@adomani
feat(data/polynomial/degree/basic): add lemmas dealing with monomials…
d9e40dc 
…, their support and their nat_degrees (#4475)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@shingtaklam1324 shingtaklam1324 shingtaklam1324 left review comments

@jcommelin jcommelin jcommelin approved these changes

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
3 participants
@adomani @jcommelin @shingtaklam1324