Skip to content

[Merged by Bors] - feat: port Combinatorics.Colex#1926

Closed
mo271 wants to merge 11 commits intomasterfrom
port/Combinatorics.Colex
Closed

[Merged by Bors] - feat: port Combinatorics.Colex#1926
mo271 wants to merge 11 commits intomasterfrom
port/Combinatorics.Colex

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Jan 29, 2023

Open in Gitpod

mo271 added 4 commits January 29, 2023 21:02
@mo271
feat: port Combinatorics.Colex
edd0647
@mo271
Initial file copy from mathport
37dda8c
@mo271
automated fixes
f6d8a37 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mo271
starting
4ceaaae
@mo271 mo271 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jan 29, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Jan 29, 2023

Currently trying to get LinearOrder (Finset.Colex α) to work...

@mo271 mo271 added help-wanted The author needs attention to resolve issues and removed WIP Work in progress labels Jan 29, 2023
@Komyyy Komyyy added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Feb 4, 2023
jcommelin
jcommelin reviewed Feb 4, 2023
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 4, 2023
@Komyyy Komyyy added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 4, 2023
jcommelin
jcommelin approved these changes Feb 4, 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 🎉

bors merge

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 4, 2023
bors bot pushed a commit that referenced this pull request Feb 4, 2023
@mo271 @Komyyy
feat: port Combinatorics.Colex (#1926)
acdd22b 
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
@bors
Copy link
Copy Markdown

bors bot commented Feb 4, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Combinatorics.Colex [Merged by Bors] - feat: port Combinatorics.Colex Feb 4, 2023
@bors bors bot closed this Feb 4, 2023
@bors bors bot deleted the port/Combinatorics.Colex branch February 4, 2023 10:37
kim-em added a commit that referenced this pull request Oct 22, 2023
@kim-em
remove all porting notes tagged #1926
1406284
This was referenced Jan 4, 2024
Merged
Closed
This was referenced Feb 17, 2026
Closed
Closed
Closed
Closed
Closed
@github-actions github-actions bot mentioned this pull request Mar 1, 2026
Closed
@github-actions github-actions bot mentioned this pull request Mar 23, 2026
Closed
@github-actions github-actions bot mentioned this pull request Apr 2, 2026
Closed
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

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.

4 participants

@mo271 @jcommelin @kim-em @Komyyy