Commit 2023-04-29 03:33 27974dac

View on Github →

feat: port LinearAlgebra.SymplecticGroup (#3696)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/SymplecticGroup.lean

added def Matrix.J

added theorem Matrix.J_det_mul_J_det

added theorem Matrix.J_inv

added theorem Matrix.J_squared

added theorem Matrix.J_transpose

added theorem Matrix.isUnit_det_J

added def Matrix.symplecticGroup

added theorem SymplecticGroup.J_mem

added theorem SymplecticGroup.coe_J

added theorem SymplecticGroup.coe_inv'

added theorem SymplecticGroup.coe_inv

added theorem SymplecticGroup.inv_eq_symplectic_inv

added theorem SymplecticGroup.inv_left_mul_aux

added theorem SymplecticGroup.mem_iff'

added theorem SymplecticGroup.mem_iff

added theorem SymplecticGroup.neg_mem

added def SymplecticGroup.symJ

added theorem SymplecticGroup.symplectic_det

added theorem SymplecticGroup.transpose_mem

added theorem SymplecticGroup.transpose_mem_iff