Skip to content

[Merged by Bors] - feat port: data.set.sigma#982

Closed
PatrickMassot wants to merge 5 commits intomasterfrom
data_set_sigma
Closed

[Merged by Bors] - feat port: data.set.sigma#982
PatrickMassot wants to merge 5 commits intomasterfrom
data_set_sigma

Conversation

@PatrickMassot
Copy link
Copy Markdown
Member

@PatrickMassot PatrickMassot commented Dec 13, 2022 •
edited
Loading

fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

@PatrickMassot PatrickMassot added the WIP Work in progress label Dec 13, 2022
@PatrickMassot
Copy link
Copy Markdown
Member Author

PatrickMassot commented Dec 13, 2022

Here I have a question about the naming convention, asked at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/referring.20to.20namespace.20in.20theorem.20name. The last commit in this PR implements the different names, it can be easily reverted.

@PatrickMassot PatrickMassot added awaiting-review and removed WIP Work in progress labels Dec 13, 2022
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. mathlib-port This is a port of a theory file from mathlib. needs-mathlib-SHA and removed awaiting-review labels Dec 13, 2022
kim-em
kim-em reviewed Dec 13, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 13, 2022

bors d+

Please merge after providing the mathlib3 sha here and in the port status wiki.

@bors
Copy link
Copy Markdown

bors bot commented Dec 13, 2022

✌️ PatrickMassot 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 13, 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 13, 2022
@PatrickMassot @kim-em
Update Mathlib/Data/Set/Sigma.lean
8a5d53b 
Co-authored-by: Scott Morrison <scott@tqft.net>
@PatrickMassot
Copy link
Copy Markdown
Member Author

PatrickMassot commented Dec 14, 2022

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

👎 Rejected by label

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Dec 14, 2022
@PatrickMassot
Copy link
Copy Markdown
Member Author

PatrickMassot commented Dec 14, 2022

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

👎 Rejected by label

@PatrickMassot PatrickMassot 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 14, 2022
@PatrickMassot
Copy link
Copy Markdown
Member Author

PatrickMassot commented Dec 14, 2022

bors merge

bors bot pushed a commit that referenced this pull request Dec 14, 2022
@PatrickMassot
feat port: data.set.sigma (#982)
c818a43 
fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat port: data.set.sigma [Merged by Bors] - feat port: data.set.sigma Dec 14, 2022
@bors bors bot closed this Dec 14, 2022
@bors bors bot deleted the data_set_sigma branch December 14, 2022 03:23
@github-actions github-actions bot mentioned this pull request Dec 14, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 15, 2022
@j-loreaux
chore(*): add mathlib4 synchronization comments (#17943)
a59dad5 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.euclidean_domain.basic`: leanprover-community/mathlib4#919
* `algebra.field.basic`: leanprover-community/mathlib4#975
* `algebra.group.opposite`: leanprover-community/mathlib4#912
* `algebra.group.prod`: leanprover-community/mathlib4#968
* `algebra.group.with_one.units`: leanprover-community/mathlib4#955
* `algebra.group_power.ring`: leanprover-community/mathlib4#979
* `algebra.hom.equiv.type_tags`: leanprover-community/mathlib4#943
* `algebra.hom.ring`: leanprover-community/mathlib4#958
* `algebra.invertible`: leanprover-community/mathlib4#930
* `algebra.order.field.canonical.basic`: leanprover-community/mathlib4#1018
* `algebra.order.field.canonical.defs`: leanprover-community/mathlib4#985
* `algebra.order.field.inj_surj`: leanprover-community/mathlib4#1017
* `algebra.order.group.densely_ordered`: leanprover-community/mathlib4#956
* `algebra.order.group.min_max`: leanprover-community/mathlib4#933
* `algebra.order.group.prod`: leanprover-community/mathlib4#1026
* `algebra.order.group.with_top`: leanprover-community/mathlib4#946
* `algebra.order.hom.monoid`: leanprover-community/mathlib4#944
* `algebra.order.monoid.prod`: leanprover-community/mathlib4#987
* `algebra.order.monoid.to_mul_bot`: leanprover-community/mathlib4#1024
* `algebra.order.ring.abs`: leanprover-community/mathlib4#929
* `algebra.order.ring.cone`: leanprover-community/mathlib4#935
* `algebra.order.sub.basic`: leanprover-community/mathlib4#936
* `algebra.order.sub.with_top`: leanprover-community/mathlib4#932
* `algebra.order.with_zero`: leanprover-community/mathlib4#903
* `combinatorics.quiver.arborescence`: leanprover-community/mathlib4#997
* `combinatorics.quiver.cast`: leanprover-community/mathlib4#990
* `control.traversable.lemmas`: leanprover-community/mathlib4#948
* `data.bool.set`: leanprover-community/mathlib4#960
* `data.int.cast.field`: leanprover-community/mathlib4#1016
* `data.int.cast.lemmas`: leanprover-community/mathlib4#995
* `data.int.cast.prod`: leanprover-community/mathlib4#1015
* `data.int.div`: leanprover-community/mathlib4#1011
* `data.int.dvd.basic`: leanprover-community/mathlib4#996
* `data.int.order.basic`: leanprover-community/mathlib4#938
* `data.nat.cast.basic`: leanprover-community/mathlib4#980
* `data.nat.cast.prod`: leanprover-community/mathlib4#1010
* `data.nat.cast.with_top`: leanprover-community/mathlib4#1019
* `data.nat.gcd.basic`: leanprover-community/mathlib4#965
* `data.nat.order.basic`: leanprover-community/mathlib4#907
* `data.nat.order.lemmas`: leanprover-community/mathlib4#927
* `data.nat.set`: leanprover-community/mathlib4#961
* `data.nat.upto`: leanprover-community/mathlib4#1020
* `data.pequiv`: leanprover-community/mathlib4#1008
* `data.set.basic`: leanprover-community/mathlib4#892
* `data.set.bool_indicator`: leanprover-community/mathlib4#988
* `data.set.image`: leanprover-community/mathlib4#949
* `data.set.n_ary`: leanprover-community/mathlib4#969
* `data.set.opposite`: leanprover-community/mathlib4#983
* `data.set.prod`: leanprover-community/mathlib4#1004
* `data.set.sigma`: leanprover-community/mathlib4#982
* `data.set_like.basic`: leanprover-community/mathlib4#993
* `data.two_pointing`: leanprover-community/mathlib4#984
* `logic.embedding.set`: leanprover-community/mathlib4#986
* `logic.equiv.embedding`: leanprover-community/mathlib4#1021
* `order.directed`: leanprover-community/mathlib4#963
* `order.rel_iso.set`: leanprover-community/mathlib4#1005
* `order.well_founded`: leanprover-community/mathlib4#970
* `ring_theory.coprime.basic`: leanprover-community/mathlib4#899



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
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

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.

2 participants

@PatrickMassot @kim-em