Commit 2023-03-16 20:41 da3fc4a3

feat(analysis/normed_space/quaternion_exponential): lemmas about the quaternion exponential (#18349) This gives the result that $\exp q = \exp r (\cos |v| + \frac{v}{|v|} \sin |v|)$ where $r$ is the real part and $v$ the imaginary part. After adding some missing algebraic lemmas, the result that $|\exp q| = |\exp r|$ is then simple.