Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(group_theory/submonoid): split into 3 files #3058

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - chore(group_theory/submonoid): split into 3 files #3058

wants to merge 18 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jun 13, 2020 •
edited

Now

  • group_theory.submonoid.basic contains the definition, complete_lattice structure, and some basic facts about closure;
  • group_theory.submonoid.operations contains definitions of various operations on submonoids;
  • group_theory.submonoid.membership contains various facts about membership in a submonoid or the submonoid closure of a set.

I want to use submonoid.closure and lemmas like monoid_hom.eq_of_eq_on_mdense before finsets etc is there.

@urkud
Copy link
Member Author

urkud commented Jun 13, 2020

Just realized that I forgot to adjust module docs. I'll do it tomorrow in the morning.

@urkud urkud added the needs-documentation This PR is missing required documentation label Jun 13, 2020
@urkud urkud added awaiting-review The author would like community review of the PR and removed needs-documentation This PR is missing required documentation labels Jun 14, 2020
bryangingechen
bryangingechen reviewed Jun 14, 2020
View reviewed changes
src/group_theory/submonoid/basic.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/default.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/default.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/default.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/default.lean Outdated Show resolved Hide resolved
@urkud @bryangingechen
Apply suggestions from code review
11fca3a 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 16, 2020
@semorrison
Copy link
Collaborator

(Just marking as changes-requested to fix the conflict, and click resolve on the one thread above after deciding whether to make further changes for it.)

@urkud urkud added the WIP Work in progress label Jun 23, 2020
@urkud
Copy link
Member Author

urkud commented Jun 23, 2020

I'm going to push the current version now. It is not ready for review, I just want CI to try to build it.

@urkud urkud changed the title chore(group_theory/submonoid): split into 2 files chore(group_theory/submonoid): split into 3 files Jun 27, 2020
@urkud urkud added awaiting-review The author would like community review of the PR and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Jun 28, 2020
sgouezel
sgouezel reviewed Jun 28, 2020
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

src/group_theory/submonoid/basic.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/basic.lean Outdated Show resolved Hide resolved
src/group_theory/submonoid/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jun 28, 2020

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

urkud and others added 3 commits June 28, 2020 17:22
@urkud
Copy link
Member Author

urkud commented Jun 28, 2020

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 28, 2020
bors bot pushed a commit that referenced this pull request Jun 28, 2020
@urkud
chore(group_theory/submonoid): split into 3 files (#3058)
2ec83dc 
Now

* `group_theory.submonoid.basic` contains the definition, `complete_lattice` structure, and some basic facts about `closure`;
* `group_theory.submonoid.operations` contains definitions of various operations on submonoids;
* `group_theory.submonoid.membership` contains various facts about membership in a submonoid or the submonoid closure of a set.
@bors
Copy link

bors bot commented Jun 28, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(group_theory/submonoid): split into 3 files [Merged by Bors] - chore(group_theory/submonoid): split into 3 files Jun 28, 2020
@bors bors bot closed this Jun 28, 2020
@bors bors bot deleted the submonoid-basic branch June 28, 2020 23:44
@bryangingechen bryangingechen mentioned this pull request Oct 6, 2020
Closed
bors bot pushed a commit that referenced this pull request Oct 6, 2020
@bryangingechen
chore(*): fix authorship for split files (#4480)
7948b5a 
A few files with missing copyright headers in #4477 came from splitting up older files, so the attribution was incorrect:
- `data/setoid/partition.lean` was split from `data/setoid.lean` in #2853.
- `data/finset/order.lean` was split from `algebra/big_operators.lean` in #3495.
- `group_theory/submonoid/operations.lean` was split from `group_theory/submonoid.lean` in  #3058.
jcommelin pushed a commit that referenced this pull request Oct 7, 2020
@bryangingechen @jcommelin
chore(*): fix authorship for split files (#4480)
466623c 
A few files with missing copyright headers in #4477 came from splitting up older files, so the attribution was incorrect:
- `data/setoid/partition.lean` was split from `data/setoid.lean` in #2853.
- `data/finset/order.lean` was split from `algebra/big_operators.lean` in #3495.
- `group_theory/submonoid/operations.lean` was split from `group_theory/submonoid.lean` in  #3058.
adomani pushed a commit that referenced this pull request Oct 7, 2020
@bryangingechen @adomani
chore(*): fix authorship for split files (#4480)
103b05a 
A few files with missing copyright headers in #4477 came from splitting up older files, so the attribution was incorrect:
- `data/setoid/partition.lean` was split from `data/setoid.lean` in #2853.
- `data/finset/order.lean` was split from `algebra/big_operators.lean` in #3495.
- `group_theory/submonoid/operations.lean` was split from `group_theory/submonoid.lean` in  #3058.
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@urkud @cipher1024
chore(group_theory/submonoid): split into 3 files (leanprover-communi…
aadce8e 
…ty#3058)

Now

* `group_theory.submonoid.basic` contains the definition, `complete_lattice` structure, and some basic facts about `closure`;
* `group_theory.submonoid.operations` contains definitions of various operations on submonoids;
* `group_theory.submonoid.membership` contains various facts about membership in a submonoid or the submonoid closure of a set.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

@jcommelin jcommelin jcommelin left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@urkud @semorrison @bryangingechen @jcommelin @sgouezel