Skip to content

[Merged by Bors] - port: Algebra.Order.Group.Abs#896

Closed
kim-em wants to merge 13 commits intomasterfrom
algebra_order_group_abs
Closed

[Merged by Bors] - port: Algebra.Order.Group.Abs#896
kim-em wants to merge 13 commits intomasterfrom
algebra_order_group_abs

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Dec 7, 2022 •
edited by Ruben-VandeVelde
Loading

a95b16cbade0f938fc24abd05412bde1e84bab9b

Issues:

  • typeclass inference
  • the absolute value notation can't cope with nesting or leading minus signs.

@kim-em kim-em added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 7, 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 7, 2022
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 7, 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 7, 2022
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Dec 7, 2022
View reviewed changes
@kim-em kim-em 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 7, 2022
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review mathlib-port This is a port of a theory file from mathlib. and removed WIP Work in progress labels Dec 7, 2022
jcommelin
jcommelin reviewed Dec 8, 2022
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Dec 8, 2022
@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 8, 2022
@Ruben-VandeVelde @jcommelin
Apply suggestions from code review
2e7e557 
Co-authored-by: Johan Commelin <johan@commelin.net>
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Dec 8, 2022

LGTM

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Dec 8, 2022

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 8, 2022
@Ruben-VandeVelde Ruben-VandeVelde removed awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Dec 8, 2022
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 9, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Dec 9, 2022
bors bot pushed a commit that referenced this pull request Dec 9, 2022
@kim-em @Ruben-VandeVelde
port: Algebra.Order.Group.Abs (#896)
d53ae16 
a95b16cbade0f938fc24abd05412bde1e84bab9b

- [x] depends on: #895 

Issues:
* typeclass inference
* the absolute value notation can't cope with nesting or leading minus signs.

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

bors bot commented Dec 9, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title port: Algebra.Order.Group.Abs [Merged by Bors] - port: Algebra.Order.Group.Abs Dec 9, 2022
@bors bors bot closed this Dec 9, 2022
@bors bors bot deleted the algebra_order_group_abs branch December 9, 2022 01:37
@github-actions github-actions bot mentioned this pull request Dec 10, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 10, 2022
chore(*): add mathlib4 synchronization comments (#17871)
eedb281 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.group.ulift`: leanprover-community/mathlib4#906
* `algebra.group.with_one.basic`: leanprover-community/mathlib4#922
* `algebra.group_with_zero.units.lemmas`: leanprover-community/mathlib4#920
* `algebra.order.field.defs`: leanprover-community/mathlib4#905
* `algebra.order.group.abs`: leanprover-community/mathlib4#896
* `algebra.order.group.inj_surj`: leanprover-community/mathlib4#916
* `algebra.order.group.type_tags`: leanprover-community/mathlib4#921
* `algebra.order.monoid.with_top`: leanprover-community/mathlib4#902
* `algebra.order.positive.ring`: leanprover-community/mathlib4#911
* `algebra.order.ring.canonical`: leanprover-community/mathlib4#905
* `algebra.order.ring.char_zero`: leanprover-community/mathlib4#905
* `algebra.order.ring.defs`: leanprover-community/mathlib4#905
* `algebra.order.ring.inj_surj`: leanprover-community/mathlib4#917
* `algebra.ring.idempotents`: leanprover-community/mathlib4#918
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

@kim-em @jcommelin @Ruben-VandeVelde