New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras #6385
Conversation
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
We do this via the normalizer of a Lie algebra, which is also defined here.
|
||
## Tags | ||
|
||
lie subalgebra, normalizer, idealizer, cartan subalgebra |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IMO Lie and Cartan should be uppercase here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I generally agree with capitalising names but I've been consistently sticking to pure lowercase for these Tags
across 15+ files so I'm reluctant to make this file the odd one out!
Of course if someone wants to submit a PR capitalising all the names in Tags
in src/algebra/lie/*.lean
then that would be fine by me :-)
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
Co-authored-by: Johan Commelin <johan@commelin.net>
The can be inferred from the (explicit) `lie_subalgebra` argument.
No functional change but perhaps helpful to a human
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
We do this via the normalizer of a Lie subalgebra, which is also defined here.
Pull request successfully merged into master. Build succeeded: |
We do this via the normalizer of a Lie subalgebra, which is also defined here.
We do this via the normalizer of a Lie subalgebra, which is also defined here.
We do this via the normalizer of a Lie subalgebra, which is also defined here.