-
Notifications
You must be signed in to change notification settings - Fork 297
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/ring): add non-unital and non-associative rings #12300
Conversation
Unfortunately add a few more steps to the hierarchy makes a few more unification problems fail, so much of this PR is patching up proofs that used to work. Hopefully none of the patches are too unpleasant? |
I'm encouraged by the fact that we seemed to need only 8 patches in a codebase with c.800k lines. Thanks for doing this. (I wonder what will happen when we want to talk about commutative non-unital rings 😨) bors merge |
Following up on #11124. The longer term goal is to develop C^* algebras, where non-unital algebras are an essential part of the theory. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed (retrying...): |
Following up on #11124. The longer term goal is to develop C^* algebras, where non-unital algebras are an essential part of the theory. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
bors merge |
Following up on #11124. The longer term goal is to develop C^* algebras, where non-unital algebras are an essential part of the theory. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Following up on #11124.
The longer term goal is to develop C^* algebras, where non-unital algebras are an essential part of the theory.