contractLeft_ι_mul — Mathlib

English

A standard left contraction identity with ι_Q a and product: for a ∈ M and 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 (\\iota_Q(a) \\cdot b) = d(a) \\cdot b - \\iota_Q(a) \\cdot (d\\lbrack b) $$$

Lean4

/-- This is [grinberg_clifford_2016][] Theorem 6 -/
theorem contractLeft_ι_mul (a : M) (b : CliffordAlgebra Q) : d⌋(ι Q a * b) = d a • b - ι Q a * (d⌋b) := by
  -- Porting note: Lean cannot figure out anymore the third argument

  refine foldr'_ι_mul _ _ ?_ _ _ _
  exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

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