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](http://en.wikipedia.org/wiki/Polar_decomposition#Matrix_polar_decomposition))


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.



Polar decomposition for quaternionic matrices?
A key wordphrase here is "[Cartan decomposition](http://en.wikipedia.org/wiki/Cartan_decomposition)". Since $G=SL\_n(\mathbb H)$ is a semisimple group, there is a diffeomorphism 
$$K\times \mathfrak p\rightarrow G$$ 
taking $(k,X)$ to $k\cdot {\rm exp}(X)$, where $K$ is a maximal compact subgroup of $G$ (i.e. the compact symplectic group) and $\mathfrak p$ is the vector subspace of ${\mathfrak sl}\_n(\mathbb H)$ fixed by the Cartan involution $X\rightarrow \bar X^t$ (the quaternionic version of Hermitian). 


