mathlib

a5b382d8 - feat(linear_algebra/symplectic_group): add definition of symplectic group (#15513)

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`. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>