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/jordan): Introduce Jordan rings #11073
Conversation
This reverts commit 0ffc566.
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.
Sorry for just leaving only these insubstantial comments -- they caught my eye when reading through to see what a Jordan ring was.
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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.
This now looks great. Thanks for coming back to it. Only some very minor formatting tweaks, then feel free to merge.
bors d+
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors r+ |
👎 Rejected by label |
Not sure why CI is failing with no logs, I've restarted it |
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.
Optional golfing suggestion.
Co-authored-by: Oliver Nash <github@olivernash.org>
bors r+ |
Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring. Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
) Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring. Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring. Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring. Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring.
Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative.
commute.lie_eq
#15675