feat(data/matrix/basic): update_{column,row}_subsingleton (#8422)

src/data/matrix/basic.lean

@@ -1263,6 +1263,22 @@ begin
   { rwa [update_column_ne h, if_neg h] }
 end
 
+@[simp] lemma update_column_subsingleton [subsingleton m] (A : matrix n m R)
+  (i : m) (b : n → R) :
+  A.update_column i b = (col b).minor id (function.const m ()) :=
+begin
+  ext x y,
+  simp [update_column_apply, subsingleton.elim i y]
+end
+
+@[simp] lemma update_row_subsingleton [subsingleton n] (A : matrix n m R)
+  (i : n) (b : m → R)  :
+  A.update_row i b = (row b).minor (function.const n ()) id :=
+begin
+  ext x y,
+  simp [update_column_apply, subsingleton.elim i x]
+end
+
 lemma map_update_row [decidable_eq n] (f : α → β) :
   map (update_row M i b) f = update_row (M.map f) i (f ∘ b) :=
 begin