Theorems · Theorem · field theory

Quaternion.expSeries_odd_of_imaginary

∀ {q : Quaternion ℝ},
  q.re = 0 →
    ∀ (n : ℕ),
      ((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n + 1)) fun x => q) =
        ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial / ‖q‖) • q

The odd terms of expSeries are real, and correspond to the series for $\frac{q}{‖q‖} \sin ‖q‖$.

Defined in

Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Cited by

1 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound