Theorems · Theorem · field theory
Quaternion.expSeries_even_of_imaginary
∀ {q : Quaternion ℝ},
q.re = 0 →
∀ (n : ℕ),
((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n)) fun x => q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n).factorial)The even terms of expSeries are real, and correspond to the series for $\cos ‖q‖$.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- mul_oneproof · cited by 3,885
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- ContinuousMultilinearMapstatement · cited by 1,016
- pow_oneproof · cited by 894
- div_eq_mul_invproof · cited by 715
- Nat.factorialstatement and proof · cited by 616
- sqproof · cited by 280
- pow_mulproof · cited by 210
Cited by1
Results whose statement or proof uses this declaration.
- Quaternion.hasSum_expSeries_of_imaginaryproof · cited by 1