contractLeft_ι — Mathlib

English

For any x ∈ M, the left contraction of ι_Q x is the algebra map applied to x: d ⌋ ι_Q x = algebraMap R (Clifford(Q)) (d x).

Русский

Для любого x ∈ M левое свёртывание ι_Q x равно алгебраическому отображению: d ⌋ ι_Q x = algebraMap(d x).

LaTeX

$$$ d\\lbrack ι_Q(x) = algebraMap R (Clifford(Q)) (d(x)) $$$

Lean4

@[simp]
theorem contractLeft_ι (x : M) : d⌋ι Q x = algebraMap R _ (d x) := by
  -- Porting note: Lean cannot figure out anymore the third argument

  refine
    (foldr'_ι _ _ ?_ _ _).trans <| by
      simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero, Algebra.algebraMap_eq_smul_one]
  exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

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