mathlib documentation


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 #

def linear_map.general_linear_group (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] :
Type u_2

The group of invertible linear maps from M to itself


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


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


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