Mathlib v3 is deprecated. Go to Mathlib v4

Def symplectic_group.sym_J

Modification history

2022-09-16 10:27

src/linear_algebra/symplectic_group.lean

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

Added symplectic_group.sym_J View on Github →