imK_add

Mathlib.Algebra.Quaternion

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem imK_add : (a + b).imK = a.imK + b.imK :=
  rfl

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

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

Разделы

Аффилиация

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