k_mul_i

Mathlib.Algebra.QuaternionBasis

URI: https://scilib.ai/kg/mathlib#QuaternionAlgebra.Basis.k_mul_i

← MathLib Explorer

English

Let q be a quaternion basis as above. Then k i = -c1 j.

Русский

Пусть q — базис кватернионной алгебры над R. Тогда k i = -c1 j.

LaTeX

$$$q.k \\cdot q.i = -c_1 \\, q.j$$$

Lean4

@[simp]
theorem k_mul_i : q.k * q.i = -c₁ • q.j :=
  by
  rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]
  linear_combination (norm := module)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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