Documentation

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Basic lemmas about the general linear group $GL(n, R)$ #

This file lists various basic lemmas about the general linear group $GL(n, R)$. For the definitions, see Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean.

source
šŸ”ø coverage
def Matrix.planeConformalMatrix {R : Type u_1} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ā‰  0) :
GL (Fin 2) R

The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of $GL_2(R)$ if a ^ 2 + b ^ 2 is nonzero.

Instances For
    source
    šŸ“ coverage
    @[simp]
    theorem Matrix.val_planeConformalMatrix {R : Type u_1} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ā‰  0) :
    ā†‘(planeConformalMatrix a b hab) = !![a, -b; b, a]
    source
    šŸ“ coverage
    theorem Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g : GL n R} :
    g āˆˆ Subgroup.center (GL n R) ā†” ā†‘g āˆˆ Set.range ā‡‘(Matrix.scalar n)

    The center of GL n R consists of scalar matrices.

    source
    šŸ“ coverage
    @[deprecated Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar (since := "2026-02-08")]
    theorem Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g : GL n R} :
    g āˆˆ Subgroup.center (GL n R) ā†” ā†‘g āˆˆ Set.range ā‡‘(Matrix.scalar n)

    Alias of Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar.

    The center of GL n R consists of scalar matrices.

    source
    šŸ“ coverage
    theorem Matrix.GeneralLinearGroup.center_eq_range_scalar {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :
    Subgroup.center (GL n R) = (scalar n).range

    The center of GL n R is the image of RĖ£.

    source
    šŸ“ coverage
    @[deprecated Matrix.GeneralLinearGroup.center_eq_range_scalar (since := "2026-02-08")]
    theorem Matrix.GeneralLinearGroup.center_eq_range_units {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :
    Subgroup.center (GL n R) = (scalar n).range

    Alias of Matrix.GeneralLinearGroup.center_eq_range_scalar.

    The center of GL n R is the image of RĖ£.