imJ_add

Mathlib.Algebra.Quaternion

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

English

The j-coordinate is additive under quaternion addition: ImJ(a + b) = ImJ(a) + ImJ(b).

Русский

Коэффициент при j распределяется по сумме: ImJ(a + b) = ImJ(a) + ImJ(b).

LaTeX

$$$$\forall a,b \in \mathbb{H}(R):\ \operatorname{Im}_J(a + b) = \operatorname{Im}_J(a) + \operatorname{Im}_J(b).$$$$

Lean4

@[simp]
theorem imJ_add : (a + b).imJ = a.imJ + b.imJ :=
  rfl

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

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

Разделы

Аффилиация

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