re_exp

Mathlib.Analysis.Normed.Algebra.QuaternionExponential

URI: https://scilib.ai/kg/mathlib#Quaternion.re_exp

English

The real part of exp(q) equals exp(re q) times the cosine of the norm of (q − re q).

Русский

Действительная часть exp(q) равна exp(re q) умноженной на cos(‖q − re q‖).

LaTeX

$$$\operatorname{Re}(\exp_{\mathbb{R}}(q)) = \exp_{\mathbb{R}}(q_{\mathrm{re}}) \cdot \cos\big\|q - q_{\mathrm{re}}\big\|.$$$

Lean4

theorem re_exp (q : ℍ[ℝ]) : (exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - q.re‖ := by simp [exp_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru