feat(linear_algebra/determinant): Show that the determinant is a mult…

…ilinear map (#5142)

src/linear_algebra/determinant.lean

@@ -8,6 +8,7 @@ import data.fintype.card
 import group_theory.perm.sign
 import algebra.algebra.basic
 import tactic.ring
+import linear_algebra.multilinear
 
 universes u v w z
 open equiv equiv.perm finset function
@@ -273,6 +274,13 @@ begin
   simp [update_column_transpose, det_transpose]
 end
 
+/-- `det` is a multilinear map over the rows of the matrix -/
+@[simps apply]
+def det_row_multilinear : multilinear_map R (λ (i : n), n → R) R :=
+{ to_fun := det,
+  map_add' := det_update_row_add,
+  map_smul' := det_update_row_smul }
+
 @[simp] lemma det_block_diagonal {o : Type*} [fintype o] [decidable_eq o] (M : o → matrix n n R) :
   (block_diagonal M).det = ∏ k, (M k).det :=
 begin