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 #

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

Instances For
    source
    def LinearMap.GeneralLinearGroup.toLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : LinearMap.GeneralLinearGroup R M) :
    M ≃ₗ[R] M

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

    Instances For
      source
      def LinearMap.GeneralLinearGroup.ofLinearEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) :
      LinearMap.GeneralLinearGroup R M

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

      Instances For
        source
        def LinearMap.GeneralLinearGroup.generalLinearEquiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
        LinearMap.GeneralLinearGroup R M ≃* M ≃ₗ[R] M

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

        Instances For
          source
          @[simp]
          theorem LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (f : LinearMap.GeneralLinearGroup R M) :
          ↑(↑(LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ↑f
          source
          @[simp]
          theorem LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (f : LinearMap.GeneralLinearGroup R M) :
          ↑(↑(LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ↑↑f