contractRight_eq — Mathlib

English

For any d ∈ Module.Dual R M and x ∈ Clifford(Q), the right contraction satisfies contractRight(x, d) = reverse (contractLeft(d) (reverse x)).

Русский

Для любого d ∈Dual R M и любого элемента x ∈ Clifford(Q) выполнено равенство контрактному правому свёртыванию: contractRight(x, d) = reverse (contractLeft(d) (reverse x)).

LaTeX

$$$ contractRight(Q, x, d) = \\mathrm{reverse} \\bigl( contractLeft(Q, d) (\\mathrm{reverse}(x)) \\bigr) $$$

Lean4

theorem contractRight_eq (x : CliffordAlgebra Q) :
    contractRight (Q := Q) x d = reverse (contractLeft (R := R) (M := M) d <| reverse x) :=
  rfl

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