mathlib

da3fc4a3 - feat(analysis/normed_space/quaternion_exponential): lemmas about the quaternion exponential (#18349)

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.