mathlib3 documentation

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 #

@[reducible]
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

Equations

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

Equations

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