invOf_ι_mul_ι_mul_ι — Mathlib

English

Another identity showing how the inverse of ι_Q(a) interacts with the product ι_Q(b) ι_Q(a) in the graded Clifford algebra, yielding the same vector as a direct polar combination.

Русский

Ещё одно тождество о том, как обратимый элемент ι_Q(a) взаимодействует с произведением ι_Q(b) ι_Q(a) в градуированной клиффордовой алгебре, приводя к вектору через полярность.

LaTeX

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

Lean4

/-- $a^{-1}ba$ is a vector. -/
theorem invOf_ι_mul_ι_mul_ι (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, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
    invOf_mul_self, one_smul]

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