ιMulti_succ_curryLeft — Mathlib

English

For any n and m ∈ M, the curryLeft of the (n+1)-ary exterior product with respect to the first argument is the left multiplication by ι_R(m) composed with the n-ary exterior product: (ιMulti R (n+1)).curryLeft m = (ι_R m) · (ιMulti R n).

Русский

Для любого n и элемента m ∈ M, карри-левый разложитель (n+1)-арной внешней продукции равен левому умножению на ι_R(m), затем применению n-арной продукции.

LaTeX

$$$ (ιMulti\\_R(n+1)).curryLeft(m) = (ι_R(m)) \\cdot (ιMulti\\_R(n)). $$$

Lean4

theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) :
    (ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R (ι R m)).compAlternatingMap (ιMulti R n) := by ext; simp

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