Packaging nonsingular matrices in the general linear group

Over a field, Matrix.GeneralLinearGroup.mkOfDetNeZero packages a matrix with nonzero determinant as an element of GL. This file records how that packaging interacts with matrix multiplication, existing general-linear elements, and transvections.

Main results

• Matrix.GeneralLinearGroup.mkOfDetNeZero_mul: packaging a matrix product agrees with multiplication in GL.
• Matrix.GeneralLinearGroup.mkOfDetNeZero_coe: repackaging the matrix of an element of GL recovers that element.
• Matrix.GeneralLinearGroup.mkOfDetNeZero_transvection: packaging a transvection recovers its canonical element of GL.

@[simp]

theorem Matrix.GeneralLinearGroup.mkOfDetNeZero_mul {n : Type u} [Fintype n] [DecidableEq n] {K : Type v} [Field K] (M N : Matrix n n K) (hM : M.det ≠ 0) (hN : N.det ≠ 0) : mkOfDetNeZero (M * N) ⋯ = mkOfDetNeZero M hM * mkOfDetNeZero N hN

Packaging a product by mkOfDetNeZero agrees with multiplication in GL.

@[simp]

theorem Matrix.GeneralLinearGroup.mkOfDetNeZero_coe {n : Type u} [Fintype n] [DecidableEq n] {K : Type v} [Field K] (A : GL n K) : mkOfDetNeZero ↑A ⋯ = A

Repackaging the matrix underlying an element of GL by mkOfDetNeZero recovers that element.

@[simp]

theorem Matrix.GeneralLinearGroup.mkOfDetNeZero_transvection {n : Type u} [Fintype n] [DecidableEq n] {K : Type v} [Field K] {i j : n} (hij : i ≠ j) (c : K) : mkOfDetNeZero (transvection i j c) ⋯ = SpecialLinearGroup.toGL (SpecialLinearGroup.transvection hij c)

Packaging a transvection matrix by mkOfDetNeZero recovers its canonical element of GL.