Documentation

Mathlib.LinearAlgebra.GeneralLinearGroup

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 #

@[reducible, inline]
abbrev LinearMap.GeneralLinearGroup (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
Type u_2

The group of invertible linear maps from M to itself

Equations
Instances For

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

    Equations
    • f.toLinearEquiv = { toLinearMap := f, invFun := f.inv.toFun, left_inv := , right_inv := }
    Instances For

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

      Equations
      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