Commit 2023-06-07 00:58 1cabfdd1

View on Github →

feat: port Analysis.NormedSpace.QuaternionExponential (#4756)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/QuaternionExponential.lean

added theorem Quaternion.exp_coe

added theorem Quaternion.exp_eq

added theorem Quaternion.exp_of_re_eq_zero

added theorem Quaternion.hasSum_expSeries_of_imaginary

added theorem Quaternion.im_exp

added theorem Quaternion.normSq_exp

added theorem Quaternion.norm_exp

added theorem Quaternion.re_exp