{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₂] →
                  (toFun : ((i : ι) → M₁ i) → M₂) →
                    (∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
                        toFun (Function.update m i (x + y)) =
                          toFun (Function.update m i x) + toFun (Function.update m i y)) →
                      (∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
                          toFun (Function.update m i (c • x)) = c • toFun (Function.update m i x)) →
                        MultilinearMap R M₁ M₂