English
Contraction by d is compatible with multiplication by scalars from the left: for any r ∈ R and Clifford element b, d ⌋ (algebraMap r · b) = algebraMap r · (d ⌋ b).
Русский
Свёртывание слева совместимо с умножением на скаляры слева: для любого r ∈ R и элемента Клиффорда b имеем \( d ⌋ (algebraMap r · b) = algebraMap r · (d ⌋ b) \).
LaTeX
$$$ d\\lbrack algebraMap R (CliffordAlgebra Q) \\; b = algebraMap R (CliffordAlgebra Q) \\; r \\cdot (d\\lbrack b) $$$
Lean4
/-- Contract an element of the clifford algebra with an element `d : Module.Dual R M` from the
right.
Note that $x ⌊ v$ is spelt `contractRight x (Q.associated v)`.
This includes [grinberg_clifford_2016][] Theorem 16.75 -/
def contractRight : CliffordAlgebra Q →ₗ[R] Module.Dual R M →ₗ[R] CliffordAlgebra Q :=
LinearMap.flip (LinearMap.compl₂ (LinearMap.compr₂ contractLeft reverse) reverse)
