Skip to content

[Merged by Bors] - feat: port Combinatorics.Quiver.Path#811

Closed
joelriou wants to merge 53 commits intomasterfrom
combinatorics_path
Closed

[Merged by Bors] - feat: port Combinatorics.Quiver.Path#811
joelriou wants to merge 53 commits intomasterfrom
combinatorics_path

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Dec 1, 2022 •
edited
Loading

Mathlib3 SHA : 62a5626868683c104774de8d85b9855234ac807c

kim-em added 30 commits November 21, 2022 11:05
kim-em and others added 13 commits December 1, 2022 04:14
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 1, 2022
@hrmacbeth hrmacbeth added the mathlib-port This is a port of a theory file from mathlib. label Dec 1, 2022
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 1, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 1, 2022

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 1, 2022
@joelriou joelriou removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 1, 2022
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Dec 1, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Dec 1, 2022
bors bot pushed a commit that referenced this pull request Dec 1, 2022
@kim-em
feat: port Combinatorics.Quiver.Path (#811)
a764138 
Mathlib3 SHA : 62a5626868683c104774de8d85b9855234ac807c

- [ ] depends on: #749
@bors
Copy link
Copy Markdown

bors bot commented Dec 1, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Combinatorics.Quiver.Path [Merged by Bors] - feat: port Combinatorics.Quiver.Path Dec 1, 2022
@bors bors bot closed this Dec 1, 2022
@bors bors bot deleted the combinatorics_path branch December 1, 2022 17:53
@github-actions github-actions bot mentioned this pull request Dec 2, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 2, 2022
chore(*): add mathlib4 synchronization comments (#17790)
02ca4ad 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.order.sub.canonical`: leanprover-community/mathlib4#814
* `category_theory.category.Rel`: leanprover-community/mathlib4#822
* `category_theory.category.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.category`: leanprover-community/mathlib4#749
* `category_theory.functor.functorial`: leanprover-community/mathlib4#822
* `category_theory.isomorphism`: leanprover-community/mathlib4#749
* `category_theory.natural_transformation`: leanprover-community/mathlib4#749
* `category_theory.thin`: leanprover-community/mathlib4#822
* `combinatorics.quiver.basic`: leanprover-community/mathlib4#749
* `combinatorics.quiver.path`: leanprover-community/mathlib4#811
* `data.psigma.order`: leanprover-community/mathlib4#815
* `data.stream.defs`: leanprover-community/mathlib4#665
* `order.boolean_algebra`: leanprover-community/mathlib4#794
* `order.heyting.basic`: leanprover-community/mathlib4#793
* `order.rel_iso.group`: leanprover-community/mathlib4#813
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 3, 2022
chore(*): add mathlib4 synchronization comments (#17790)
308f6d0 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.order.sub.canonical`: leanprover-community/mathlib4#814
* `category_theory.category.Rel`: leanprover-community/mathlib4#822
* `category_theory.category.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.basic`: leanprover-community/mathlib4#749
* `category_theory.functor.category`: leanprover-community/mathlib4#749
* `category_theory.functor.functorial`: leanprover-community/mathlib4#822
* `category_theory.isomorphism`: leanprover-community/mathlib4#749
* `category_theory.natural_transformation`: leanprover-community/mathlib4#749
* `category_theory.thin`: leanprover-community/mathlib4#822
* `combinatorics.quiver.basic`: leanprover-community/mathlib4#749
* `combinatorics.quiver.path`: leanprover-community/mathlib4#811
* `data.psigma.order`: leanprover-community/mathlib4#815
* `data.stream.defs`: leanprover-community/mathlib4#665
* `order.boolean_algebra`: leanprover-community/mathlib4#794
* `order.heyting.basic`: leanprover-community/mathlib4#793
* `order.rel_iso.group`: leanprover-community/mathlib4#813
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.

4 participants

@joelriou @kim-em @ChrisHughes24 @hrmacbeth