mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

feat: Lie algebra root spaces are 1-dimensional

Open ocfnash opened this issue 1 year ago • 1 comments

over a field of characteristic zero, when the Killing form is non-singular

  • [ ] depends on: #13076

Open in Gitpod

ocfnash avatar May 15 '24 20:05 ocfnash

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#13076~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 21 '24 20:05 leanprover-community-mathlib4-bot

Thank you for the very helpful review!

ocfnash avatar May 22 '24 08:05 ocfnash

Thanks :tada:

bors merge

jcommelin avatar May 22 '24 12:05 jcommelin

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 22 '24 12:05 mathlib-bors[bot]