Skip to content

[Merged by Bors] - feat: port Order.BooleanAlgebra#794

Closed
kim-em wants to merge 25 commits intomasterfrom
BooleanAlgebra
Closed

[Merged by Bors] - feat: port Order.BooleanAlgebra#794
kim-em wants to merge 25 commits intomasterfrom
BooleanAlgebra

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Nov 30, 2022 •
edited
Loading

mathlib3 sha 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

@kim-em kim-em added WIP Work in progress please-adopt Inactive PR (would be valuable to adopt) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Nov 30, 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 added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 1, 2022
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 1, 2022

This PR/issue depends on:

@ChrisHughes24 ChrisHughes24 added awaiting-review and removed WIP Work in progress please-adopt Inactive PR (would be valuable to adopt) labels Dec 2, 2022
kim-em
kim-em commented Dec 2, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 2, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 2, 2022
bors bot pushed a commit that referenced this pull request Dec 2, 2022
@kim-em @Ruben-VandeVelde @ChrisHughes24
feat: port Order.BooleanAlgebra (#794)
608fd2f 
mathlib3 sha 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

- [x] depends on: #793 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 2, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Order.BooleanAlgebra [Merged by Bors] - feat: port Order.BooleanAlgebra Dec 2, 2022
@bors bors bot closed this Dec 2, 2022
@bors bors bot deleted the BooleanAlgebra branch December 2, 2022 17:26
@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

@kim-em @hrmacbeth @ChrisHughes24 @Ruben-VandeVelde