Polar decomposition on $\mathbf{GL}(n,\mathbb{R})$

Question

I am asked to prove that for $g\in\mathbf{GL}(n,\mathbb{R})$, $g$ can be unique written as $$g=k_1 \begin{pmatrix} a_1 & & 0\\ & \ddots &\\ 0 & & a_n \end{pmatrix} k_2, k_1,k_2\in\mathbf{O}(n,\mathbb{R}), a_1\geq a_2\geq\dots\geq a_n>0$$.

I think this is somehow related to the polar decomposition mentioned in Axler's linear algebra done right, however I have no exact idea how to do it concisely. Any help or recommended reading?

Answer 1

The factorization in question is a special case of the matrix version of the singular value decomposition. See Theorem 7.77 in the forthcoming fourth edition of Linear Algebra Done Right. Chapter 7 of this forthcoming new edition is freely available at https://linear.axler.net/.