im_star

Mathlib.Algebra.Quaternion

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

English

Let a be a quaternion; the imaginary part after conjugation is the negation of the original imaginary part: (star a).im = - a.im.

Русский

Пусть a — кватернион; воображаемая часть после сопряжения равна противоположной исходной: (star a).im = - a.im.

LaTeX

$$$ (star a).im = - a.im $$$

Lean4

@[simp]
theorem im_star : (star a).im = -a.im :=
  QuaternionAlgebra.im_star a

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

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

Разделы

Аффилиация

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