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(linear_algebra/symplectic_group): add definition of symplectic group #15513
Conversation
I've golfed a few proofs a bit and I removed the simp-attribute for |
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
…roup (#15513) This PR defines the symplectic group over arbitrary ring (with characteristic not 2) It also moves the definition of the `symplectic.J` into the new `linear_algebra/symplectic_group` file, and adds a lemma `from_blocks_neg` to `data/matrix/block`. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Build failed (retrying...): |
…roup (#15513) This PR defines the symplectic group over arbitrary ring (with characteristic not 2) It also moves the definition of the `symplectic.J` into the new `linear_algebra/symplectic_group` file, and adds a lemma `from_blocks_neg` to `data/matrix/block`. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Pull request successfully merged into master. Build succeeded: |
…roup (#15513) This PR defines the symplectic group over arbitrary ring (with characteristic not 2) It also moves the definition of the `symplectic.J` into the new `linear_algebra/symplectic_group` file, and adds a lemma `from_blocks_neg` to `data/matrix/block`. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
This PR defines the symplectic group over arbitrary ring (with characteristic not 2)
It also moves the definition of the
symplectic.J
into the newlinear_algebra/symplectic_group
file, and adds a lemmafrom_blocks_neg
todata/matrix/block
.Co-authored-by: Moritz Doll moritz.doll@googlemail.com