j_mul_k — Mathlib

English

Let q be the basis. Then the product j k equals (c2 c3) times the unit element minus c3 times i, i.e., j k = (c2 c3) 1 − c3 i.

Русский

Пусть q — базис. Тогда j k = (c2 c3)·1 − c3·i.

LaTeX

$$$q.j \\cdot q.k = (c_2 c_3) \\cdot 1 - c_3 \\cdot q.i$$$

Lean4

@[simp]
theorem j_mul_k : q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i :=
  by
  rw [← i_mul_j, ← mul_assoc, j_mul_i, sub_mul, smul_mul_assoc, j_mul_j, ← smul_assoc, k_mul_j]
  rfl

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