feat(determinant): towards multilinearity (#3887)

From the sphere eversion project. In a PR coming soon, this will be used to prove that the determinant of a family of vectors in a given basis is multi-linear (see [here](https://github.com/leanprover-community/sphere-eversion/blob/2c776f6a92c0f9babb521a02ab0cc341a06d3f3c/src/vec_det.lean) for a preview if needed).

Author: PatrickMassot

src/linear_algebra/determinant.lean

@@ -7,6 +7,7 @@ import data.matrix.pequiv
 import data.fintype.card
 import group_theory.perm.sign
 import ring_theory.algebra
+import tactic.ring
 
 universes u v w z
 open equiv equiv.perm finset function
@@ -223,4 +224,49 @@ end
 
 end det_zero
 
+lemma det_update_column_add (M : matrix n n R) (j : n) (u v : n → R) :
+  det (update_column M j $ u + v) = det (update_column M j u) + det (update_column M j v) :=
+begin
+  simp only [det],
+  have : ∀ σ : perm n, ∏ i, M.update_column j (u + v) (σ i) i =
+                       ∏ i, M.update_column j u (σ i) i + ∏ i, M.update_column j v (σ i) i,
+  { intros σ,
+    simp only [update_column_apply, prod_ite, filter_eq',
+               finset.prod_singleton, finset.mem_univ, if_true, pi.add_apply, add_mul] },
+  rw [← sum_add_distrib],
+  apply sum_congr rfl,
+  intros x _,
+  rw [this, mul_add]
+end
+
+lemma det_update_row_add (M : matrix n n R) (j : n) (u v : n → R) :
+  det (update_row M j $ u + v) = det (update_row M j u) + det (update_row M j v) :=
+begin
+  rw [← det_transpose, ← update_column_transpose, det_update_column_add],
+  simp [update_column_transpose, det_transpose]
+end
+
+lemma det_update_column_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
+  det (update_column M j $ s • u) = s * det (update_column M j u) :=
+begin
+  simp only [det],
+  have : ∀ σ : perm n, ∏ i, M.update_column j (s • u) (σ i) i = s * ∏ i, M.update_column j u (σ i) i,
+  { intros σ,
+    simp only [update_column_apply, prod_ite, filter_eq', finset.prod_singleton, finset.mem_univ,
+               if_true, algebra.id.smul_eq_mul, pi.smul_apply],
+    ring },
+  rw mul_sum,
+  apply sum_congr rfl,
+  intros x _,
+  rw this,
+  ring
+end
+
+lemma det_update_row_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
+  det (update_row M j $ s • u) = s * det (update_row M j u) :=
+begin
+  rw [← det_transpose, ← update_column_transpose, det_update_column_smul],
+  simp [update_column_transpose, det_transpose]
+end
+
 end matrix