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.

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

[Merged by Bors] - feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative #12231

Closed
wants to merge 11 commits into from

Conversation

dupuisf
Copy link
Collaborator

@dupuisf dupuisf commented Feb 23, 2022

We show that if a set of elements of a subobject commute, its closure/adjoin is also commutative The subobjects include (additive) submonoids, (additive) subgroups, subsemirings, subrings, and subalgebras.


Open in Gitpod

@dupuisf dupuisf added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Feb 23, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Feb 23, 2022
@dupuisf dupuisf 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 Feb 27, 2022
@dupuisf dupuisf added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 4, 2022
@dupuisf dupuisf changed the title feat(ring_theory/adjoin/basic): if some elements of an algebra commute, the algebra they generate is commutative feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative Mar 4, 2022
@riccardobrasca
Copy link
Member

Thanks!

bors d+

@bors
Copy link

bors bot commented Mar 4, 2022

✌️ dupuisf 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 delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Mar 4, 2022
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
src/group_theory/subgroup/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/subsemiring/basic.lean Outdated Show resolved Hide resolved
@dupuisf
Copy link
Collaborator Author

dupuisf commented Mar 5, 2022

bors r+

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Mar 5, 2022
bors bot pushed a commit that referenced this pull request Mar 5, 2022
…ommute, its closure/adjoin is also commutative (#12231)

We show that if a set of elements of a subobject commute, its closure/adjoin is also commutative The subobjects include (additive) submonoids, (additive) subgroups, subsemirings, subrings, and subalgebras.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 5, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative [Merged by Bors] - feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative Mar 5, 2022
@bors bors bot closed this Mar 5, 2022
@bors bors bot deleted the dupuisf/adjoin_comm branch March 5, 2022 01:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions. 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
Development

Successfully merging this pull request may close these issues.

None yet

3 participants