ι_mul_ι_mul_ι — Mathlib

English

A triple product ι_Q a ι_Q b ι_Q a can be expressed as a Clifford image of a linear combination of a and b given by the polar form.

Русский

Тройной продукт ι_Q a ι_Q b ι_Q a равен изображению Клиффордовой алгебры соответствующей линейной комбинации a и b, задаваемой полярной формой.

LaTeX

$$$ι_Q a ι_Q b ι_Q a = ι_Q (polar(Q)(a,b) \\cdot a - Q(a) \\cdot b)$$$

Lean4

/-- $aba$ is a vector. -/
theorem ι_mul_ι_mul_ι (a b : M) : ι Q a * ι Q b * ι Q a = ι Q (QuadraticMap.polar Q a b • a - Q a • b) := by
  rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ← Algebra.smul_def, ←
    map_smul, ← map_smul, ← map_sub]

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