star_im

Mathlib.Algebra.Quaternion

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

English

The conjugation fixes the real part and negates the imaginary part: star a.im = - a.im.

Русский

Сопряжение сохраняет вещественную часть и обращает знак мнимой части: star a.im = - a.im.

LaTeX

$$$ star a.im = - a.im $$$

Lean4

@[simp]
theorem star_im : star a.im = -a.im := by ext <;> simp

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

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

Разделы

Аффилиация

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