# mathlib3documentation

linear_algebra.general_linear_group

# The general linear group of linear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See also matrix.general_linear_group

## Main definitions #

• linear_map.general_linear_group
@[reducible]
def linear_map.general_linear_group (R : Type u_1) (M : Type u_2) [semiring R] [ M] :
Type u_2

The group of invertible linear maps from M to itself

Equations
@[protected, instance]
def linear_map.general_linear_group.has_coe_to_fun {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
(λ (_x : , M M)
Equations
def linear_map.general_linear_group.to_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [ M] (f : M) :

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

Equations
def linear_map.general_linear_group.of_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [ M] (f : M ≃ₗ[R] M) :

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

Equations

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

Equations
@[simp]
@[simp]
theorem linear_map.general_linear_group.coe_fn_general_linear_equiv (R : Type u_1) (M : Type u_2) [semiring R] [ M] (f : M) :