Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(lie/semisimple): tweak lie_algebra.subsingleton_of_semisimple_lie_abelian #8728

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(lie/semisimple): tweak lie_algebra.subsingleton_of_semisimple_lie_abelian #8728

wants to merge 1 commit into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Aug 17, 2021

Open in Gitpod

@ocfnash ocfnash added the awaiting-review The author would like community review of the PR label Aug 17, 2021
@ocfnash ocfnash requested a review from jcommelin August 17, 2021 18:38
jcommelin
jcommelin approved these changes Aug 17, 2021
View reviewed changes
Copy link
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

@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 Aug 17, 2021
bors bot pushed a commit that referenced this pull request Aug 17, 2021
@ocfnash
chore(lie/semisimple): tweak `lie_algebra.subsingleton_of_semisimple_…
e6e5718 
…lie_abelian` (#8728)
@bors
Copy link

bors bot commented Aug 17, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(lie/semisimple): tweak lie_algebra.subsingleton_of_semisimple_lie_abelian [Merged by Bors] - chore(lie/semisimple): tweak lie_algebra.subsingleton_of_semisimple_lie_abelian Aug 17, 2021
@bors bors bot closed this Aug 17, 2021
@bors bors bot deleted the lie_ss_abel branch August 17, 2021 22:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

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.
2 participants
@ocfnash @jcommelin