English
The matrix of rotation a on the basis of 1 and i is the conformal matrix with entries re(a), -im(a); im(a), re(a).
Русский
Матрица вращения a в базисе 1, i равна конформной матрице с элементами re(a), -im(a); im(a), re(a).
LaTeX
$$$\text{toMatrix}_{basisOneI,basisOneI}(\text{rotation}(a)) = \text{planeConformalMatrix}(\Re a, \Im a)$$$
Lean4
/-- The matrix representation of `rotation a` is equal to the conformal matrix
`!![re a, -im a; im a, re a]`. -/
theorem toMatrix_rotation (a : Circle) :
LinearMap.toMatrix basisOneI basisOneI (rotation a).toLinearEquiv =
Matrix.planeConformalMatrix (re a) (im a) (by simp [pow_two, ← normSq_apply]) :=
by
ext i j
simp only [LinearMap.toMatrix_apply, coe_basisOneI, LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv,
rotation_apply, coe_basisOneI_repr, mul_re, mul_im, Matrix.val_planeConformalMatrix, Matrix.of_apply,
Matrix.cons_val', Matrix.empty_val', Matrix.cons_val_fin_one]
fin_cases i <;> fin_cases j <;> simp
