The General Linear group $GL(n, R)$ #
This file defines the elements of the General Linear group
general_linear_group n R,
consisting of all invertible
Main definitions #
matrix.general_linear_groupis the type of matrices over R which are units in the matrix ring.
matrix.GL_posgives the subgroup of matrices with positive determinant (over a linear ordered ring).
matrix group, group, matrix inverse
The determinant of a unit matrix is itself a unit.
GL n R and
general_linear_group R n groups are multiplicatively equivalent
Given a matrix with unit determinant we get an element of
GL n R
This is the subgroup of
nxn matrices with entries over a
linear ordered ring and positive determinant.
Formal operation of negation on general linear group on even cardinality
n given by negating
special_linear_group n R embeds into
GL_pos n R