∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ} (m : M),
  (ExteriorAlgebra.ιMulti R n.succ).curryLeft m =
    (LinearMap.mulLeft R ((ExteriorAlgebra.ι R) m)).compAlternatingMap (ExteriorAlgebra.ιMulti R n)