exp_eq — Mathlib

English

For q ∈ ℍ[ℝ] with q.re = 0, the exponential is exp(q) = cos(‖q‖) + (sin(‖q‖)/‖q‖) q.

Русский

Для мнимого кватерниона q (re q = 0) экспонента равна cos‖q‖ + (sin‖q‖/‖q‖) q.

LaTeX

$$$\exp_{\mathbb{R}}(q) = \uparrow\big(\cos \|q\|\big) + \big(\dfrac{\sin \|q\|}{\|q\|}\big) q$$$

Lean4

/-- The closed form for the quaternion exponential on arbitrary quaternions. -/
theorem exp_eq (q : Quaternion ℝ) : exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) :=
  by
  rw [← exp_of_re_eq_zero q.im q.re_im, ← coe_mul_eq_smul, ← exp_coe, ← exp_add_of_commute, re_add_im]
  exact Algebra.commutes q.re (_ : ℍ[ℝ])

Похожие утверждения