contractLeft_mul_algebraMap — Mathlib

English

A standard left contraction rule: for a ∈ M, b ∈ Clifford(Q), d ⌋ (ι_Q a · b) = d(a) · b − ι_Q a · (d ⌋ b).

Русский

Пояснение к левому свёртыванию: для a ∈ M, b ∈ Clifford(Q) имеем $ d ⌋ (ι_Q a · b) = d(a) · b − ι_Q a · (d ⌋ b) $.

LaTeX

$$$ d\\lbrack ι_Q(a) \\cdot b = d(a) \\cdot b - ι_Q(a) \\cdot (d\\lbrack b) $$$

Lean4

theorem contractLeft_mul_algebraMap (a : CliffordAlgebra Q) (r : R) :
    d⌋(a * algebraMap _ _ r) = d⌋a * algebraMap _ _ r := by
  rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes]

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