norm_exp — Mathlib

English

The norm of exp(q) equals the norm of exp(re q).

Русский

Норма экспоненты экспоненты равна норме экспоненты вещественной части: \|exp(q)\| = \|exp(q_{re})\|.

LaTeX

$$$\|\exp_{\mathbb{R}}(q)\| = \|\exp_{\mathbb{R}}(q_{\mathrm{re}})\|.$$$

Lean4

/-- Note that this implies that exponentials of pure imaginary quaternions are unit quaternions
since in that case the RHS is `1` via `NormedSpace.exp_zero` and `norm_one`. -/
@[simp]
theorem norm_exp (q : ℍ[ℝ]) : ‖exp ℝ q‖ = ‖exp ℝ q.re‖ := by
  rw [norm_eq_sqrt_real_inner (exp ℝ q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]

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