Skip to content

[Merged by Bors] - feat: port Order.Disjoint#773

Closed
hrmacbeth wants to merge 12 commits intomasterfrom
hrmacbeth-order-disjoint
Closed

[Merged by Bors] - feat: port Order.Disjoint#773
hrmacbeth wants to merge 12 commits intomasterfrom
hrmacbeth-order-disjoint

Conversation

@hrmacbeth
Copy link
Copy Markdown
Member

@hrmacbeth hrmacbeth commented Nov 28, 2022 •
edited
Loading

sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

@kim-em kim-em added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Nov 28, 2022
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Nov 28, 2022
@hrmacbeth hrmacbeth added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 28, 2022
Ruben-VandeVelde
Ruben-VandeVelde reviewed Nov 28, 2022
View reviewed changes
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Nov 28, 2022
@hrmacbeth hrmacbeth added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 28, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 28, 2022

Looks good, thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 28, 2022
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@hrmacbeth @kim-em
feat: port Order.Disjoint (#773)
a2a8dbe 
sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@hrmacbeth @kim-em
feat: port Order.Disjoint (#773)
68eb464 
sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@hrmacbeth @kim-em
feat: port Order.Disjoint (#773)
4449a0a 
sha 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 28, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Order.Disjoint [Merged by Bors] - feat: port Order.Disjoint Nov 28, 2022
@bors bors bot closed this Nov 28, 2022
@bors bors bot deleted the hrmacbeth-order-disjoint branch November 28, 2022 22:47
rosborn added a commit that referenced this pull request Nov 29, 2022
@rosborn
Merge branch 'master' into Control.Monad.Basic
5b25af6 
* master: (26 commits)
  docs (Order.BoundedOrder): fix typos (#775)
  feat: port Algebra.Order.Monoid.Cancel.Defs (#774)
  feat: port Order.Disjoint (#773)
  feat: port linarith (#526)
  feat: port Algebra.Order.Monoid.Defs (#771)
  feat: port control.functor (#612)
  feat(Algebra/GroupWithZero/Commute): port file (#762)
  feat: port Logic.Equiv.Option (#674)
  chore: fix todos in `to_additive` (#765)
  feat(Algebra/Order/Monoid/MinMax): port file (#763)
  fix: update context in recursive calls in split_ifs (#761)
  feat(Algebra/Regular/Basic): port file (#758)
  feat: port Order.BoundedOrder (#697)
  feat: port Data.Pi.Algebra (#564)
  feat: port Algebra.Hom.Embedding (#764)
  fix: to_additive generates equation lemmas for target (#767)
  fix: fix translation errors in various files (#716)
  fix: remove submodules (#766)
  feat(Algebra/Group/Commute): port file (#750)
  feat(Algebra/Ring/Commute): port file (#759)
  ...
@github-actions github-actions bot mentioned this pull request Nov 29, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 1, 2022
chore(*): add mathlib4 synchronization comments (#17754)
8d89a80 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.field.defs`: leanprover-community/mathlib4#668
* `algebra.group.commute`: leanprover-community/mathlib4#750
* `algebra.group_with_zero.commute`: leanprover-community/mathlib4#762
* `algebra.group_with_zero.semiconj`: leanprover-community/mathlib4#757
* `algebra.group_with_zero.units.basic`: leanprover-community/mathlib4#735
* `algebra.hom.embedding`: leanprover-community/mathlib4#764
* `algebra.order.monoid.cancel.defs`: leanprover-community/mathlib4#774
* `algebra.order.monoid.canonical.defs`: leanprover-community/mathlib4#778
* `algebra.order.monoid.defs`: leanprover-community/mathlib4#771
* `algebra.order.monoid.min_max`: leanprover-community/mathlib4#763
* `algebra.order.monoid.order_dual`: leanprover-community/mathlib4#786
* `algebra.order.sub.defs`: leanprover-community/mathlib4#732
* `algebra.regular.basic`: leanprover-community/mathlib4#758
* `algebra.ring.commute`: leanprover-community/mathlib4#759
* `algebra.ring.regular`: leanprover-community/mathlib4#795
* `algebra.ring.semiconj`: leanprover-community/mathlib4#751
* `control.applicative`: leanprover-community/mathlib4#798
* `control.functor`: leanprover-community/mathlib4#612
* `control.monad.basic`: leanprover-community/mathlib4#752
* `data.countable.defs`: leanprover-community/mathlib4#736
* `data.int.units`: leanprover-community/mathlib4#807
* `data.nat.basic`: leanprover-community/mathlib4#729
* `data.nat.psub`: leanprover-community/mathlib4#806
* `data.nat.units`: leanprover-community/mathlib4#805
* `data.pi.algebra`: leanprover-community/mathlib4#564
* `data.prod.lex`: leanprover-community/mathlib4#783
* `logic.embedding.basic`: leanprover-community/mathlib4#700
* `logic.equiv.option`: leanprover-community/mathlib4#674
* `order.bounded_order`: leanprover-community/mathlib4#697
* `order.with_bot`: leanprover-community/mathlib4#776
* `order.disjoint`: leanprover-community/mathlib4#773
* `order.min_max`: leanprover-community/mathlib4#728
* `order.prop_instances`: leanprover-community/mathlib4#792
* `order.rel_iso.basic`: leanprover-community/mathlib4#772
@github-actions github-actions bot mentioned this pull request Dec 2, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

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.

3 participants

@hrmacbeth @kim-em @Ruben-VandeVelde