refactor(linear_algebra/nonsingular_inverse, data/matrix/basic): update_* rectangular matrices (#3403)

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: pechersky

src/data/matrix/basic.lean

@@ -740,6 +740,61 @@ lemma row_mul_vec [semiring α] (M : matrix m n α) (v : n → α) :
 
 end row_col
 
+section update
+
+/-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`. -/
+def update_row [decidable_eq n] (M : matrix n m α) (i : n) (b : m → α) : matrix n m α :=
+function.update M i b
+
+/-- Update, i.e. replace the `i`th column of matrix `A` with the values in `b`. -/
+def update_column [decidable_eq m] (M : matrix n m α) (j : m) (b : n → α) : matrix n m α :=
+λ i, function.update (M i) j (b i)
+
+variables {M : matrix n m α} {i : n} {j : m} {b : m → α} {c : n → α}
+
+@[simp] lemma update_row_self [decidable_eq n] : update_row M i b i = b :=
+function.update_same i b M
+
+@[simp] lemma update_column_self [decidable_eq m] : update_column M j c i j = c i :=
+function.update_same j (c i) (M i)
+
+@[simp] lemma update_row_ne [decidable_eq n] {i' : n} (i_ne : i' ≠ i) :
+  update_row M i b i' = M i' := function.update_noteq i_ne b M
+
+@[simp] lemma update_column_ne [decidable_eq m] {j' : m} (j_ne : j' ≠ j) :
+  update_column M j c i j' = M i j' := function.update_noteq j_ne (c i) (M i)
+
+lemma update_row_val [decidable_eq n] {i' : n} :
+  update_row M i b i' j = if i' = i then b j else M i' j :=
+begin
+  by_cases i' = i,
+  { rw [h, update_row_self, if_pos rfl] },
+  { rwa [update_row_ne h, if_neg h] }
+end
+
+lemma update_column_val [decidable_eq m] {j' : m} : update_column M j c i j' = if j' = j then c i else M i j' :=
+begin
+  by_cases j' = j,
+  { rw [h, update_column_self, if_pos rfl] },
+  { rwa [update_column_ne h, if_neg h] }
+end
+
+lemma update_row_transpose [decidable_eq m] : update_row Mᵀ j c = (update_column M j c)ᵀ :=
+begin
+  ext i' j,
+  rw [transpose_val, update_row_val, update_column_val],
+  refl
+end
+
+lemma update_column_transpose [decidable_eq n] : update_column Mᵀ i b = (update_row M i b)ᵀ :=
+begin
+  ext i' j,
+  rw [transpose_val, update_row_val, update_column_val],
+  refl
+end
+
+end update
+
 end matrix
 
 namespace ring_hom

src/linear_algebra/nonsingular_inverse.lean

@@ -49,51 +49,6 @@ variables {n : Type u} [fintype n] [decidable_eq n] {α : Type v}
 open_locale matrix big_operators
 open equiv equiv.perm finset
 
-
-section update
-
-/-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`. -/
-def update_row (A : matrix n n α) (i : n) (b : n → α) : matrix n n α :=
-function.update A i b
-
-/-- Update, i.e. replace the `i`th column of matrix `A` with the values in `b`. -/
-def update_column (A : matrix n n α) (j : n) (b : n → α) : matrix n n α :=
-λ i, function.update (A i) j (b i)
-
-variables {A : matrix n n α} {i j : n} {b : n → α}
-
-@[simp] lemma update_row_self : update_row A i b i = b := function.update_same i b A
-
-@[simp] lemma update_column_self : update_column A j b i j = b i := function.update_same j (b i) (A i)
-
-@[simp] lemma update_row_ne {i' : n} (i_ne : i' ≠ i) : update_row A i b i' = A i' :=
-function.update_noteq i_ne b A
-
-@[simp] lemma update_column_ne {j' : n} (j_ne : j' ≠ j) : update_column A j b i j' = A i j' :=
-function.update_noteq j_ne (b i) (A i)
-
-lemma update_row_val {i' : n} : update_row A i b i' j = if i' = i then b j else A i' j :=
-begin
-  by_cases i' = i,
-  { rw [h, update_row_self, if_pos rfl] },
-  { rw [update_row_ne h, if_neg h] }
-end
-
-lemma update_column_val {j' : n} : update_column A j b i j' = if j' = j then b i else A i j' :=
-begin
-  by_cases j' = j,
-  { rw [h, update_column_self, if_pos rfl] },
-  { rw [update_column_ne h, if_neg h] }
-end
-
-lemma update_row_transpose : update_row Aᵀ i b = (update_column A i b)ᵀ :=
-begin
-  ext i' j,
-  rw [transpose_val, update_row_val, update_column_val],
-  refl
-end
-end update
-
 section cramer
 /-!
   ### `cramer` section
@@ -170,7 +125,7 @@ begin
   { -- i = j: this entry should be `A.det`
     rw [if_pos h, ←h],
     congr, ext i',
-    by_cases h : i' = i, { rw [h, update_row_self] }, { rw [update_row_ne h]} },
+    by_cases h : i' = i, { rw [h, update_row_self] }, { rw [update_row_ne h] } },
   { -- i ≠ j: this entry should be 0
     rw [if_neg h],
     apply det_zero_of_column_eq h,