curryLeft_same — Mathlib

English

Let f be an alternating multilinear map of arity n+2. For any m in M, applying curryLeft by the same element twice yields the zero map.

Русский

Пусть f — чередующаяся многолинейная карта степени n+2. Для любого m в M повторное создание CurryLeft по одному и тому же элементу даёт нулевую карту.

LaTeX

$$$$\forall f \in \operatorname{Alt}^{n+2}_R(M,N), \forall m \in M:\ (f\text{\text{ curryLeft }} m)\text{\text{ curryLeft }} m = 0.$$$$

Lean4

/-- Currying with the same element twice gives the zero map. -/
@[simp]
theorem curryLeft_same (f : M [⋀^Fin n.succ.succ]→ₗ[R] N) (m : M) : (f.curryLeft m).curryLeft m = 0 :=
  ext fun _ => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one

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