contractLeftAux_contractLeftAux — Mathlib

English

For every vector v ∈ M and Clifford elements x, fx, the contraction by the left auxiliary map satisfies contractLeftAux(d)(v)(ι_Q(v) x, contractLeftAux(d)(x, fx)) = Q(v) · fx.

Русский

Пусть v ∈ M и элементы клиффордовой алгебры x, fx. Тогда неравенство левого вспомогательного отображения даёт: contractLeftAux(d)(v)(ι_Q(v) x, contractLeftAux(d)(x, fx)) = Q(v) · fx.

LaTeX

$$$ contractLeftAux(Q, d)\\,v\\bigl(\\iota_Q(v)\\, x, \\; contractLeftAux(Q, d)\\,v (x, f_x)\\bigr) = Q(v) \\cdot f_x $$$

Lean4

theorem contractLeftAux_contractLeftAux (v : M) (x : CliffordAlgebra Q) (fx : CliffordAlgebra Q) :
    contractLeftAux Q d v (ι Q v * x, contractLeftAux Q d v (x, fx)) = Q v • fx :=
  by
  simp only [contractLeftAux_apply_apply]
  rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self, zero_add]

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