Skip to content

[Merged by Bors] - feat: port Data.Polynomial.EraseLead#2721

Closed
ChrisHughes24 wants to merge 4 commits intomasterfrom
port/Data.Polynomial.EraseLead
Closed

[Merged by Bors] - feat: port Data.Polynomial.EraseLead#2721
ChrisHughes24 wants to merge 4 commits intomasterfrom
port/Data.Polynomial.EraseLead

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Mar 8, 2023

Open in Gitpod

@ChrisHughes24
feat: port Data.Polynomial.EraseLead
3df6907
@ChrisHughes24
Initial file copy from mathport
7e3a6ee
@ChrisHughes24
automated fixes
f70b2d6 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@ChrisHughes24
fixes
011a3a3
@ChrisHughes24 ChrisHughes24 added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Mar 8, 2023
jcommelin
jcommelin approved these changes Mar 8, 2023
View reviewed changes
Copy link
Copy Markdown
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 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Mar 8, 2023

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin jcommelin added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 8, 2023
@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Mar 8, 2023
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Mar 8, 2023

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Mar 8, 2023
bors bot pushed a commit that referenced this pull request Mar 8, 2023
@ChrisHughes24
feat: port Data.Polynomial.EraseLead (#2721)
c7d26d4
@bors
Copy link
Copy Markdown

bors bot commented Mar 8, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Polynomial.EraseLead [Merged by Bors] - feat: port Data.Polynomial.EraseLead Mar 8, 2023
@bors bors bot closed this Mar 8, 2023
@bors bors bot deleted the port/Data.Polynomial.EraseLead branch March 8, 2023 14:58
bustercopley added a commit that referenced this pull request Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
400cc88 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley added a commit that referenced this pull request Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
d8d37cc 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley added a commit that referenced this pull request Oct 22, 2023
@bustercopley
Update dependencies for CI (do not merge)
6a3c135 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
bustercopley pushed a commit that referenced this pull request Oct 22, 2023
@bustercopley
Update dependencies for CI (do not merge)
3665052 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ChrisHughes24 @jcommelin @kim-em