Basic lemmas about the general linear group #
This file lists various basic lemmas about the general linear group LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
.
The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of
a ^ 2 + b ^ 2
is nonzero.
Equations
- Matrix.planeConformalMatrix a b hab = Matrix.GeneralLinearGroup.mkOfDetNeZero !![a, -b; b, a] ⋯