curryLeft_compAlternatingMap — Mathlib

English

Let g be a linear map and f an alternating map. The curryLeft operation commutes with post-composition by g: curryLeft of g∘f equals g∘curryLeft f.

Русский

Пусть g — линейное отображение, а f — чередующаяся карта. Операция curryLeft коммутирует с пост-композицией: curryLeft(g∘f) = g∘curryLeft(f).

LaTeX

$$$$\forall (g: N \to N_2)\ (f: M [⋀^Fin n.succ]→ₗ[R] N)\ (m: M),\ (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m).$$$$

Lean4

@[simp]
theorem curryLeft_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) :
    (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m) :=
  rfl

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