# mathlib3documentation

analysis.normed_space.quaternion_exponential

# Lemmas about exp on quaternions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains results about exp on quaternion ℝ.

## Main results #

• quaternion.exp_eq: the general expansion of the quaternion exponential in terms of real.cos and real.sin.
• quaternion.exp_of_re_eq_zero: the special case when the quaternion has a zero real part.
• quaternion.norm_exp: the norm of the quaternion exponential is the norm of the exponential of the real part.
@[simp, norm_cast]
theorem quaternion.exp_coe (r : ) :
r = (exp r)
theorem quaternion.has_sum_exp_series_of_imaginary {q : quaternion } (hq : q.re = 0) {c s : } (hc : has_sum (λ (n : ), (-1) ^ n * q ^ (2 * n) / ((2 * n).factorial)) c) (hs : has_sum (λ (n : ), (-1) ^ n * q ^ (2 * n + 1) / ((2 * n + 1).factorial)) s) :
has_sum (λ (n : ), n) (λ (_x : fin n), q)) (c + (s / q) q)

Auxiliary result; if the power series corresponding to real.cos and real.sin evaluated at ‖q‖ tend to c and s, then the exponential series tends to c + (s / ‖q‖).

theorem quaternion.exp_of_re_eq_zero (q : quaternion ) (hq : q.re = 0) :

The closed form for the quaternion exponential on imaginary quaternions.

The closed form for the quaternion exponential on arbitrary quaternions.

@[simp]

Note that this implies that exponentials of pure imaginary quaternions are unit quaternions since in that case the RHS is 1 via exp_zero and norm_one.