Partitioned inverse, off-diagonal row entries: $((GG^\top)^{-1})_{i,j} = -\big((HH^\top)^{-1}Hg\big)_{j}\,((GG^\top)^{-1})_{ii}$

Let $G \in \mathbb{R}^{(n+1)\times k}$, fix a row index $i$, let $g = G_{i,:}$ be the $i$-th row and $H \in \mathbb{R}^{n\times k}$ the matrix of the remaining rows in their original order, and assume $HH^\top$ is invertible. Let $c = (HH^\top)^{-1}Hg \in \mathbb{R}^n$ be the least-squares coefficients of $g$ on the rows of $H$. Then for every $a \in \{1,\dots,n\}$, writing $i \oplus a$ for the index in $G$ of the $a$-th row of $H$,

Together with the diagonal formula $((GG^\top)^{-1})_{ii} = 1/(g^\top g - (Hg)^\top(HH^\top)^{-1}Hg)$ (schur_diag_inv), this describes the whole $i$-th row of $(GG^\top)^{-1}$: it equals $Q^{-1}(1, -c^\top)$ (in the ordering $i$ first), with $Q$ the Schur complement. It is the deterministic step that turns off-diagonal entries of an inverse Wishart matrix into a ratio of independent quantities (regression coefficients over a residual).

Formalization Note. The index $i\oplus a$ is i.succAbove a and $H$ is G.submatrix i.succAbove id. Lean's matrix inverse is total; the identity holds under the sole hypothesis $\det(HH^\top)\ne 0$, including the degenerate case $Q = 0$, where $GG^\top$ is singular and both sides are $0$.