k_mul_j

Mathlib.Algebra.QuaternionBasis

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

English

Let q be the quaternion basis. Then k j = c3 j? No: k j = c3 i.

Русский

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

LaTeX

$$$q.k \\cdot q.j = c_3 \\cdot q.i$$$

Lean4

@[simp]
theorem k_mul_j : q.k * q.j = c₃ • q.i := by rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]

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

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

Разделы

Аффилиация

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