# The general linear group of linear maps #

The general linear group is defined to be the group of invertible linear maps from M to itself.

See also Matrix.GeneralLinearGroup

## Main definitions #

• LinearMap.GeneralLinearGroup
@[reducible]
def LinearMap.GeneralLinearGroup (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
Type u_2

The group of invertible linear maps from M to itself

Equations
Instances For
def LinearMap.GeneralLinearGroup.toLinearEquiv {R : Type u_1} {M : Type u_2} [] [] [Module R M] (f : ) :

An invertible linear map f determines an equivalence from M to itself.

Equations
• = let __src := f; { toLinearMap := __src, invFun := f.inv.toFun, left_inv := , right_inv := }
Instances For
def LinearMap.GeneralLinearGroup.ofLinearEquiv {R : Type u_1} {M : Type u_2} [] [] [Module R M] (f : M ≃ₗ[R] M) :

An equivalence from M to itself determines an invertible linear map.

Equations
• = { val := f, inv := (), val_inv := , inv_val := }
Instances For

The general linear group on R and M is multiplicatively equivalent to the type of linear equivalences between M and itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap (R : Type u_1) (M : Type u_2) [] [] [Module R M] (f : ) :
= f
@[simp]
theorem LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv (R : Type u_1) (M : Type u_2) [] [] [Module R M] (f : ) :
= f