Commit 2022-09-16 10:27 a5b382d8
View on Github →feat(linear_algebra/symplectic_group): add definition of symplectic group (#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.