re_add_im

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.re_add_im

English

For any quaternion z, z = re(z) + im(z) I, recovering z from its real and imaginary parts.

Русский

Для любого кватерниона z верно z = re(z) + im(z) I, т.е. восстановление z по действительной и мнимой частям.

LaTeX

$$$z = \mathrm{re}(z) + \mathrm{im}(z) \cdot I$$$

Lean4

@[simp, rclike_simps]
theorem re_add_im (z : K) : (re z : K) + im z * I = z :=
  RCLike.re_add_im_ax z

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

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

Разделы

Аффилиация

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