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.

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

• Matrix.planeConformalMatrix a b hab = Matrix.GeneralLinearGroup.mkOfDetNeZero !![a, -b; b, a] ⋯

@[simp]

theorem Matrix.val_planeConformalMatrix {R : Type u_1} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : ↑(Matrix.planeConformalMatrix a b hab) = !![a, -b; b, a]