star_eq_two_re_sub

Mathlib.Algebra.Quaternion

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

English

Conjugate equals twice the real part minus the quaternion: star a = 2 Re(a) − a.

Русский

Сопряжение равняется удвоенной вещественной части минус кватернион: star a = 2 Re(a) − a.

LaTeX

$$$ star\ a = 2\, a.re - a $$$

Lean4

theorem star_eq_two_re_sub : star a = ↑(2 * a.re) - a := by simpa using QuaternionAlgebra.star_eq_two_re_sub a

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

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

Разделы

Аффилиация

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