Skip to content

[Merged by Bors] - feat: port Data.Pi.Algebra#564

Closed
joneugster wants to merge 34 commits intomasterfrom
JE/Data.Pi.Algebra
Closed

[Merged by Bors] - feat: port Data.Pi.Algebra#564
joneugster wants to merge 34 commits intomasterfrom
JE/Data.Pi.Algebra

Conversation

@joneugster
Copy link
Copy Markdown
Contributor

@joneugster joneugster commented Nov 10, 2022 •
edited
Loading

Mathlib SHA: 17a9f8f7a4ef32ee65d418103367cf30e84e631d

Done with the reviews. This should hopefully now be ready to merge.

@joneugster joneugster added help-wanted The author needs attention to resolve issues WIP Work in progress labels Nov 10, 2022
@digama0 digama0 added the mathlib-port This is a port of a theory file from mathlib. label Nov 13, 2022
@joneugster joneugster added the please-adopt Inactive PR (would be valuable to adopt) label Nov 14, 2022
@joneugster joneugster removed the please-adopt Inactive PR (would be valuable to adopt) label Nov 15, 2022
joneugster
joneugster commented Nov 16, 2022
View reviewed changes
joneugster
joneugster commented Nov 16, 2022
View reviewed changes
@joneugster joneugster added awaiting-review blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Nov 16, 2022
@joneugster joneugster added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 24, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 24, 2022

This PR/issue depends on:

@joneugster joneugster requested a review from kim-em November 25, 2022 16:22
kim-em
kim-em reviewed Nov 25, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 25, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 25, 2022
View reviewed changes
kim-em
kim-em reviewed Nov 25, 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 25, 2022
@joneugster joneugster added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 28, 2022
kim-em
kim-em reviewed Nov 28, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 28, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 28, 2022
bors bot pushed a commit that referenced this pull request Nov 28, 2022
@joneugster @kim-em
feat: port Data.Pi.Algebra (#564)
c2db4e5 
- [x] depends on: #579 

Mathlib SHA: 17a9f8f7a4ef32ee65d418103367cf30e84e631d

Done with the reviews. This should hopefully now be ready to merge.

Co-authored-by: Jon <jon.eugster@gmx.ch>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@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 Data.Pi.Algebra [Merged by Bors] - feat: port Data.Pi.Algebra Nov 28, 2022
@bors bors bot closed this Nov 28, 2022
@bors bors bot deleted the JE/Data.Pi.Algebra branch November 28, 2022 16:05
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.

5 participants

@joneugster @kim-em @Ruben-VandeVelde @digama0 @j-loreaux