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 group, group, matrix inverse
GL n R is the group of
R-matrices with unit determinant.
Defined as a subtype of matrices
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 invertible determinant we get an element of
GL n R
Given a matrix with unit determinant we get an element of
GL n R
Given a matrix with non-zero determinant over a field, we get an element of
GL n K
@[ext] as the
ext tactic already solves this.
An element of the matrix general linear group on
(n) [fintype n] can be considered as an
element of the endomorphism general linear group on
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
GL is the same as coercing striaght to a
The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of
a ^ 2 + b ^ 2 is nonzero.
This instance is here for convenience, but is not the simp-normal form.