k_mul_k — Mathlib

English

In the same setup, k squared is a scalar: k^2 = - (c1 c3) times the identity.

Русский

В той же конфигурации, квадрат k является скалярной величиной: k^2 = - (c1 c3)·1.

LaTeX

$$$q.k \\cdot q.k = -((c_1 \\cdot c_3) \\cdot 1)$$$

Lean4

@[simp]
theorem k_mul_k : q.k * q.k = -((c₁ * c₃) • (1 : A)) :=
  by
  rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ← mul_assoc, i_mul_i,
    add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm, smul_mul_assoc, mul_assoc, j_mul_j,
    add_mul, smul_mul_assoc, j_mul_j, smul_smul, smul_mul_assoc, mul_assoc, j_mul_j]
  linear_combination (norm := module)

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