i_mul_k — Mathlib

English

Let q be a basis of a quaternion algebra over a commutative ring R with parameters c1, c2, c3 ∈ R. Then the product of i and k is given by i k = c1 j + c2 k.

Русский

Пусть q является базисом кватернионовой алгебры над кольцом R с параметрами c1, c2, c3 ∈ R. Тогда произведение i и k задаётся как i k = c1 j + c2 k.

LaTeX

$$$i k = c_1\\, j + c_2\\, k$$$

Lean4

@[simp]
theorem i_mul_k : q.i * q.k = c₁ • q.j + c₂ • q.k := by
  rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]

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