Commit 2023-05-23 22:59 ccccfcfc

View on Github →

feat: port LinearAlgebra.Matrix.GeneralLinearGroup (#4265)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

added theorem Matrix.GLPos.coe_neg

added theorem Matrix.GLPos.coe_neg_GL

added theorem Matrix.GLPos.coe_neg_apply

added theorem Matrix.GLPos.det_ne_zero

added def Matrix.GLPos

added theorem Matrix.GeneralLinearGroup.coe_inv

added theorem Matrix.GeneralLinearGroup.coe_mul

added theorem Matrix.GeneralLinearGroup.coe_one

added theorem Matrix.GeneralLinearGroup.coe_toLinear

added def Matrix.GeneralLinearGroup.det

added theorem Matrix.GeneralLinearGroup.ext

added theorem Matrix.GeneralLinearGroup.ext_iff

added def Matrix.GeneralLinearGroup.mk'

added def Matrix.GeneralLinearGroup.mkOfDetNeZero

added def Matrix.GeneralLinearGroup.toLin

added def Matrix.GeneralLinearGroup.toLinear

added theorem Matrix.GeneralLinearGroup.toLinear_apply

added def Matrix.SpecialLinearGroup.coeToGL

added theorem Matrix.SpecialLinearGroup.coeToGL_det

added theorem Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix

added theorem Matrix.SpecialLinearGroup.coe_GLPos_neg

added theorem Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det

added def Matrix.SpecialLinearGroup.toGLPos

added theorem Matrix.SpecialLinearGroup.toGLPos_injective

added theorem Matrix.mem_glpos

added def Matrix.planeConformalMatrix

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean