star_add_self'

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionAlgebra.star_add_self'

English

The star-sum of a with itself also equals the embedding of twice the real part plus c2 times the imaginary part: star a + a = ↑(2 a.re + c2 a.imI).

Русский

Звездообразная сумма star a + a равна embedding ↑(2 a.re + c2 a.imI).

LaTeX

$$$\star a + a = \uparrow (2 \cdot a.re + c_2 \cdot a.imI)$$$

Lean4

theorem star_add_self' : star a + a = ↑(2 * a.re + c₂ * a.imI) := by rw [add_comm, self_add_star']

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

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

Разделы

Аффилиация

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