∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : DecidableEq ι] (f : ((i : ι) → M₁ i) → M₂)
  (h₁ :
    autoParam
      (∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
        f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
      MultilinearMap.mk'._auto_1)
  (h₂ :
    autoParam
      (∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
        f (Function.update m i (c • x)) = c • f (Function.update m i x))
      MultilinearMap.mk'._auto_3)
  (a : (i : ι) → M₁ i), (MultilinearMap.mk' f h₁ h₂) a = f a