Skip to content

[Merged by Bors] - feat: a supremum of semisimple modules is semisimple#10086

Closed
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/compl_lattice
Closed

[Merged by Bors] - feat: a supremum of semisimple modules is semisimple#10086
ocfnash wants to merge 2 commits intomasterfrom
ocfnash/compl_lattice

Conversation

@ocfnash
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash commented Jan 28, 2024 •
edited
Loading

Another small step toward Jordan-Chevalley-Dunford.

Open in Gitpod

@ocfnash ocfnash added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jan 28, 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 Jan 28, 2024
jcommelin
jcommelin reviewed Jan 29, 2024
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 29, 2024
@ocfnash ocfnash mentioned this pull request Jan 30, 2024
Closed
1 task
@ocfnash ocfnash added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 30, 2024
jcommelin
jcommelin approved these changes Feb 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 ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2024
@ocfnash
feat: a supremum of semisimple modules is semisimple (#10086)
2e5fa83 
Another small step toward Jordan-Chevalley-Dunford.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: a supremum of semisimple modules is semisimple [Merged by Bors] - feat: a supremum of semisimple modules is semisimple Feb 1, 2024
@mathlib-bors mathlib-bors bot closed this Feb 1, 2024
@mathlib-bors mathlib-bors bot deleted the ocfnash/compl_lattice branch February 1, 2024 07:10
@eric-wieser eric-wieser mentioned this pull request Feb 1, 2024
Closed
2 tasks
eric-wieser added a commit that referenced this pull request Feb 1, 2024
@eric-wieser
refactor: move lemmas with a multiset dependency to a new file
8b0c503 
This reworks the location of the lemmas from #10086.
@eric-wieser eric-wieser mentioned this pull request Feb 1, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2024
@eric-wieser
refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset…
e64d0a1 
… dependency to a new file (#10165)

This reworks the location of the lemmas from #10086, by moving them to a new `Mathlib.Order.CompactlyGenerated.Intervals` file.
The existing `Mathlib.Order.CompactlyGenerated` is moved to `Mathlib.Order.CompactlyGenerated.Basic` for consistency.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

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.

2 participants

@ocfnash @jcommelin