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: port Combinatorics.Additive.SalemSpencer #4128

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: port Combinatorics.Additive.SalemSpencer #4128

wants to merge 14 commits into from

Conversation

Parcly-Taxel
Copy link
Collaborator

@Parcly-Taxel Parcly-Taxel commented May 20, 2023 •
edited by github-actions bot

@Parcly-Taxel
feat: port Analysis.Convex.StrictConvexSpace
92a607b
@Parcly-Taxel
Initial file copy from mathport
d6e7cf5
@Parcly-Taxel
automated fixes
dff485c 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Parcly-Taxel
1 error
5bcb710
@Parcly-Taxel
Fix last error
9919a1d
@Parcly-Taxel
feat: port Combinatorics.Additive.SalemSpencer
c83e05a
@Parcly-Taxel
Initial file copy from mathport
202a412
@Parcly-Taxel
automated fixes
6493202 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Parcly-Taxel
Merge branch 'port/Analysis.Convex.StrictConvexSpace' into port/Combi…
114be6a 
…natorics.Additive.SalemSpencer
@Parcly-Taxel
Fix errors
87b8b93
@Parcly-Taxel Parcly-Taxel added blocked-by-other-PR This PR depends on another PR which is still in the queue. awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. awaiting-CI labels May 20, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label May 20, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@ChrisHughes24
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 20, 2023
bors bot pushed a commit that referenced this pull request May 20, 2023
@Parcly-Taxel @ChrisHughes24
feat: port Combinatorics.Additive.SalemSpencer (#4128)
52ae305 
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link

bors bot commented May 20, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port Combinatorics.Additive.SalemSpencer [Merged by Bors] - feat: port Combinatorics.Additive.SalemSpencer May 20, 2023
@bors bors bot closed this May 20, 2023
@bors bors bot deleted the port/Combinatorics.Additive.SalemSpencer branch May 20, 2023 12:08
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@Parcly-Taxel @ChrisHughes24 @qawbecrdtey
feat: port Combinatorics.Additive.SalemSpencer (leanprover-community#…
6d71f36 
…4128)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
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
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.

None yet
3 participants
@Parcly-Taxel @semorrison @ChrisHughes24