Skip to content

[Merged by Bors] - feat: define the trace / killing forms on a Lie algebra#6308

Closed
ocfnash wants to merge 12 commits intomasterfrom
ocfnash/killing
Closed

[Merged by Bors] - feat: define the trace / killing forms on a Lie algebra#6308
ocfnash wants to merge 12 commits intomasterfrom
ocfnash/killing

Conversation

@ocfnash
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash commented Aug 2, 2023

Open in Gitpod

@ocfnash ocfnash added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Aug 2, 2023
@ocfnash ocfnash requested a review from kbuzzard August 2, 2023 15:43
eric-wieser
eric-wieser reviewed Aug 2, 2023
View reviewed changes
@ocfnash @eric-wieser
Update Mathlib/Algebra/Lie/Killing.lean
c25877d 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
eric-wieser reviewed Aug 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Aug 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Aug 2, 2023
View reviewed changes
ocfnash and others added 3 commits August 2, 2023 18:08
@ocfnash @eric-wieser
Update Mathlib/Algebra/Lie/Killing.lean
02b549f 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ocfnash @eric-wieser
Update Mathlib/Algebra/Lie/Killing.lean
5fcdb4c 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ocfnash @eric-wieser
Update Mathlib/Algebra/Lie/Killing.lean
b395a03 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
ocfnash
ocfnash commented Aug 2, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Aug 3, 2023
View reviewed changes
@ocfnash @eric-wieser
Update Mathlib/Algebra/Lie/Killing.lean
6e43f6a 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
eric-wieser approved these changes Aug 3, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

LGTM, but maybe Kevin should take a quick look too!

ocfnash
ocfnash commented Aug 3, 2023
View reviewed changes
@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Aug 3, 2023

LGTM, but maybe Kevin should take a quick look too!

Thanks for the review!

kbuzzard
kbuzzard approved these changes Aug 9, 2023
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 looks great to me!

eric-wieser
eric-wieser approved these changes Aug 13, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser 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+

Thanks!

@bors
Copy link
Copy Markdown

bors bot commented Aug 13, 2023

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 13, 2023
@ocfnash ocfnash added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 14, 2023
@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 Aug 14, 2023
@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Aug 14, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 14, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Aug 14, 2023

bors r-

(shuffling some bors batches)

@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Canceled.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Aug 14, 2023

bors r+

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
21da7a2
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
36b5419
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
328d869
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
44375d8
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
ac406ca
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
feat: define the trace / killing forms on a Lie algebra (#6308)
23eea43
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: define the trace / killing forms on a Lie algebra [Merged by Bors] - feat: define the trace / killing forms on a Lie algebra Aug 14, 2023
@bors bors bot closed this Aug 14, 2023
@bors bors bot deleted the ocfnash/killing branch August 14, 2023 23:54
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
feat: define the trace / killing forms on a Lie algebra (#6308)
55c3561
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
feat: define the trace / killing forms on a Lie algebra (#6308)
d199d47
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
feat: define the trace / killing forms on a Lie algebra (#6308)
fdcdb11
kim-em pushed a commit that referenced this pull request Aug 17, 2023
@ocfnash @kim-em
feat: define the trace / killing forms on a Lie algebra (#6308)
d031753
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

3 participants

@ocfnash @eric-wieser @kbuzzard