imI_add

Mathlib.Algebra.Quaternion

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

English

The i-coordinate of a + b is the sum of the i-coordinates: ImI(a + b) = ImI(a) + ImI(b).

Русский

Коэффициент при i в сумме равен сумме коэффициентов при i: ImI(a + b) = ImI(a) + ImI(b).

LaTeX

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

Lean4

@[simp]
theorem imI_add : (a + b).imI = a.imI + b.imI :=
  rfl

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

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

Разделы

Аффилиация

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