feat(linear_algebra/basic): curry is linear_equiv (#3012)

Currying provides a linear_equiv. This can be used to show that
matrix lookup is a linear operation. This should allow to easily
provide a finite_dimensional instance for matrices.



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: pechersky

src/linear_algebra/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
+Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Yakov Pechersky
 -/
 import algebra.pi_instances
 import data.finsupp
@@ -1641,6 +1641,24 @@ rfl
 
 end prod
 
+section uncurry
+
+variables (V V₂ R)
+
+/-- Linear equivalence between a curried and uncurried function.
+  Differs from `tensor_product.curry`. -/
+protected def uncurry :
+  (V → V₂ → R) ≃ₗ[R] (V × V₂ → R) :=
+{ add := λ _ _, by { ext z, cases z, refl },
+  smul := λ _ _, by { ext z, cases z, refl },
+  .. equiv.arrow_arrow_equiv_prod_arrow _ _ _}
+
+@[simp] lemma coe_uncurry : ⇑(linear_equiv.uncurry R V V₂) = uncurry := rfl
+
+@[simp] lemma coe_uncurry_symm : ⇑(linear_equiv.uncurry R V V₂).symm = curry := rfl
+
+end uncurry
+
 section
 variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂}
 variables (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M) (e : M ≃ₗ[R] M₂)