Diagonal matrices with reciprocal $q_k$, $p_k$ entries are symplectic

Let $d_1,\dots,d_{2n}$ be real numbers indexed by the coordinates $q_1,\dots,q_n,p_1,\dots,p_n$ of $\mathbb R^{2n}$, and suppose

Then the diagonal matrix $D=\mathrm{diag}(d)$ is symplectic: $DJ_0D^T=J_0$, i.e. $D\in\mathrm{Sp}(2n,\mathbb R)$.

These diagonal matrices form the standard maximal torus of $\mathrm{Sp}(2n,\mathbb R)$ (independent scalings $q_k\mapsto\lambda_kq_k$, $p_k\mapsto\lambda_k^{-1}p_k$), a basic family of explicit symplectic matrices.

Formalization Note. $\mathbb R^{2n\times2n}$ is Mat n (real matrices indexed by Fin n ⊕ Fin n, first block $q$, second block $p$) and $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ is Matrix.J; IsSymplectic A is membership in Matrix.symplecticGroup, i.e. $AJ_0A^T=J_0$. The diagonal entries are a function d : Fin n ⊕ Fin n → ℝ, with $d_{q_k}$ = d (Sum.inl k) and $d_{p_k}$ = d (Sum.inr k), and $D$ is Matrix.diagonal d.