(R : Type uR) →
  {ι : Type uι} →
    (M₂ : Type v₂) →
      (M₃ : Type v₃) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : AddCommMonoid M₃] →
              [inst_3 : Module R M₂] →
                [inst_4 : Module R M₃] → [Subsingleton ι] → ι → (M₂ →ₗ[R] M₃) ≃ MultilinearMap R (fun x => M₂) M₃