Skip to content

[Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals#14460

Closed
jjaassoonn wants to merge 38 commits intomasterfrom
zjj/twosidedIdeal-operations
Closed

[Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals#14460
jjaassoonn wants to merge 38 commits intomasterfrom
zjj/twosidedIdeal-operations

Conversation

@jjaassoonn
Copy link
Copy Markdown
Collaborator

@jjaassoonn jjaassoonn commented Jul 5, 2024 •
edited
Loading

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 5, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 5, 2024 •
edited
Loading

PR summary 7db0c648ef

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.TwoSidedIdeal.BigOperators 589
Mathlib.RingTheory.TwoSidedIdeal.Operations 830

Declarations diff

+ asIdeal
+ asIdealOpposite
+ coe_asIdeal
+ finsetProd_mem
+ finsetSum_mem
+ fromIdeal
+ gc
+ ker
+ listProd_mem
+ listSum_mem
+ map
+ map_mono
+ mem_asIdeal
+ mem_asIdealOpposite
+ mem_comap
+ mem_fromIdeal
+ mem_ker
+ mem_span_iff
+ mem_span_iff_mem_addSubgroup_closure
+ mem_span_iff_mem_addSubgroup_closure_absorbing
+ mem_span_iff_mem_addSubgroup_closure_nonunital
+ multiSetProd_mem
+ multisetSum_mem
+ orderIsoIdeal
+ set_mul_subset
+ span
+ span_mono
+ subset_mul_set
+ subset_span
++ comap

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@jjaassoonn jjaassoonn added the t-algebra Algebra (groups, rings, fields, etc) label Jul 5, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 17, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 17, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2024
kim-em
kim-em reviewed Jul 18, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 18, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 18, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 18, 2024
View reviewed changes
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 18, 2024
@jjaassoonn jjaassoonn added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 22, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 22, 2024
j-loreaux
j-loreaux reviewed Jul 23, 2024
View reviewed changes
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 23, 2024
@jjaassoonn jjaassoonn added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 19, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 19, 2024
@jjaassoonn
Copy link
Copy Markdown
Collaborator Author

jjaassoonn commented Sep 19, 2024

@jjaassoonn can you fix the build error and address these comments if you have time? If you don't have time, I'm happy to help out.

So sorry for the delay, I was away. Now everything builds! Thanks for the help!

@jjaassoonn jjaassoonn removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2024
kbuzzard
kbuzzard approved these changes Sep 20, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

This all looks fine to me. I've made some mostly superficial comments. Thanks a lot!

jjaassoonn and others added 4 commits September 20, 2024 10:13
@jjaassoonn @kbuzzard
Apply suggestions from code review
c412675 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@jjaassoonn @github-actions
Update Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
1921dc8 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
doc
2b3b56a
Merge branch 'zjj/twosidedIdeal-operations' of https://github.com/lea…
03dfdab 
…nprover-community/mathlib4 into zjj/twosidedIdeal-operations
@jjaassoonn jjaassoonn requested a review from kbuzzard September 20, 2024 09:50
j-loreaux
j-loreaux reviewed Sep 23, 2024
View reviewed changes
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Sep 24, 2024

Thanks!

Maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 24, 2024

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 24, 2024
jcommelin
jcommelin reviewed Oct 1, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 1, 2024
@jjaassoonn @j-loreaux
feat(RingTheory/TwoSidedIdeal): add some basic operations on two-side…
26ad5ce 
…d-ideals (#14460)


Co-authored-by: Jireh Loreaux <oreaujy@gmail.com>




Co-authored-by: zjj <zjj@zjj>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals [Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals Oct 1, 2024
@mathlib-bors mathlib-bors bot closed this Oct 1, 2024
@mathlib-bors mathlib-bors bot deleted the zjj/twosidedIdeal-operations branch October 1, 2024 14:56
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@jjaassoonn @j-loreaux @fbarroero
feat(RingTheory/TwoSidedIdeal): add some basic operations on two-side…
f76cf72 
…d-ideals (#14460)


Co-authored-by: Jireh Loreaux <oreaujy@gmail.com>




Co-authored-by: zjj <zjj@zjj>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@eric-wieser eric-wieser mentioned this pull request May 9, 2025
Closed
@kckennylau kckennylau mentioned this pull request Jan 4, 2026
Open
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

@jcommelin jcommelin jcommelin left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@jjaassoonn @kbuzzard @kim-em @jcommelin @j-loreaux @leanprover-community-bot-assistant