ι_mul_ι_mul_invOf_ι — Mathlib

English

A version of the relation aba^{-1} is again a Clifford vector, showing how conjugation by ι_Q(a) preserves the vector-space structure up to grading.

Русский

Версия отношения aba^{-1} снова даёт вектор клиффордовой алгебры, демонстрируя, что конъюгация по ι_Q(a) сохраняет структурe векторного пространства с учётом градации.

LaTeX

$$ι_mul_ι_mul_invOf_ι(Q,a,b)$$

Lean4

/-- $aba^{-1}$ is a vector. -/
theorem ι_mul_ι_mul_invOf_ι (a b : M) [Invertible (ι Q a)] [Invertible (Q a)] :
    ι Q a * ι Q b * ⅟(ι Q a) = ι Q ((⅟(Q a) * QuadraticMap.polar Q a b) • a - b) := by
  rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul, invOf_mul_self,
    one_smul]

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