A non-zero complex number can be uniquely written in polar form as $re^{i\theta}$. There is an analogous result for complex matrices: any invertible complex matrix can be uniquely written as $UP$, where $U$ is a unitary matrix and $P$ is a positive definite Hermitian matrix (see e.g. the description on Wikipedia)
Suppose we consider $n\times n$ invertible matrices over the quaternions. Is there an analogous polar decomposition?
Or to ask the question a little more colorfully, can we complete the following list?
- roots of unity: positive reals
- unitary matrices: positive definite matrices
- compact symplectic matrices: ???
PS: Note that there exists a polar decomposition for quaternions; I'm interested in the result for matrices of quaternions.