im_exp — Mathlib

English

The imaginary part of exp(q) is exp(re q) times (sin(‖q‖)/‖q‖) times the imaginary part of q.

Русский

Мнимая часть exp(q) равна exp(re q) умножить на (sin‖q‖/‖q‖) на мнимую часть q.

LaTeX

$$$\operatorname{Im}(\exp_{\mathbb{R}}(q)) = \exp_{\mathbb{R}}(q_{\mathrm{re}}) \cdot \Big(\dfrac{\sin \|q_{\mathrm{im}}\|}{\|q_{\mathrm{im}}\|}\Big) \; q_{\mathrm{im}}.$$$

Lean4

theorem im_exp (q : ℍ[ℝ]) : (exp ℝ q).im = (exp ℝ q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im := by
  simp [exp_eq, smul_smul]

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