I found this paper on Rodrigues' rotation formula for $4$ dimensions, but I don't really see the connection to the $3$-dimensional formula. What I want to know, given orthogonal unit vectors $a_0,a_1\in\mathbf{R}^4$ and some $v\in\mathbf{R}^4$, how do I rotate $v$ around $(a_0,a_1)$ by $\pi/2$? In other words, assuming $v$ is a unit vector and orthogonal to $\langle a_0,a_1\rangle$ (the other cases should be easy to derive), how do I (efficiently) find the unit vector $v_\text{rot}$ orthogonal to $\langle a_0,a_1,v\rangle$ such that $\det(a_0,a_1,v,v_\text{rot})=1$? I believe this should uniquely determine $v_\text{rot}$?
What I got so far is that I believe I can compute $v_\text{rot}$ as $$(v_\text{rot})_j:=\sum_{\pi\in S_4:\pi(4)=j}\text{sgn}(\pi)\prod_{i=1}^{3}A_{\pi(i),i}$$ for $A:=(a_0,a_1,v)$ because this is the unique vector $d$ such that $\det(a_0,a_1,v,w)=\langle d,w\rangle$ and to maximize this inner product while keeping $\|w\|=1$ the solution is $w=d$, is that correct? If yes, is this already the fastest algorithm? Rodrigues' formula seems to be optimized for $\mathbf{R}^3$ while my approach would work in any dimension, which makes me think that it's probably not the best.