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 LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean.

source
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.

Equations
Instances For
    source
    @[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]