English
For any field R and elements a, b in R, the matrix [a, -b; b, a] represents multiplication by a + bi and is in GL2(R) exactly when a^2 + b^2 ≠ 0; its determinant equals a^2 + b^2.
Русский
Для поля R и элементов a, b ∈ R матрица \begin{pmatrix} a & -b \\ b & a \end{pmatrix} реализует умножение на a + bi и принадлежит GL2(R) тогда, когда a^2 + b^2 ≠ 0; determinant равен a^2 + b^2.
LaTeX
$$\det\begin{pmatrix} a & -b \\ b & a \end{pmatrix} = a^2 + b^2 \neq 0$$
Lean4
/-- 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. -/
@[simps! -fullyApplied val]
def planeConformalMatrix {R} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : Matrix.GeneralLinearGroup (Fin 2) R :=
GeneralLinearGroup.mkOfDetNeZero !![a, -b; b, a]
(by simpa [det_fin_two, sq] using hab)
/- TODO: Add Iwasawa matrices `n_x=!![1,x; 0,1]`, `a_t=!![exp(t/2),0;0,exp(-t/2)]` and
`k_θ=!![cos θ, sin θ; -sin θ, cos θ]`
-/
