re_add_im — Mathlib

English

For any quaternion a, the quaternion is the sum of its real part (embedded as a quaternion) and its imaginary part: a = ι(Re(a)) + Im(a).

Русский

Для любого кватерниона a кватернион равен сумме своей действительной части (встроенной как кватернион) и мнимой части: a = ι(Re(a)) + Im(a).

LaTeX

$$$\iota(\operatorname{Re}(a)) + \operatorname{Im}(a) = a$$$

Lean4

@[simp]
theorem re_add_im : ↑a.re + a.im = a :=
  QuaternionAlgebra.ext (add_zero _) (zero_add _) (zero_add _) (zero_add _)

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