∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ)
  [inst_3 : DecidableEq (Fin n)] (m : Fin n → M) (i : Fin n) (c : R) (x : M),
  ((MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun x => ExteriorAlgebra.ι R).toFun
      (Function.update m i (c • x)) =
    c •
      ((MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun x => ExteriorAlgebra.ι R).toFun
        (Function.update m i x)