feat(linear_algebra/matrix/nonsingular_inverse): lemmas about adjugate (

#9947)

src/linear_algebra/matrix/determinant.lean

@@ -333,6 +333,17 @@ begin
   simp [update_row_transpose, det_transpose]
 end
 
+lemma det_update_row_smul' (M : matrix n n R) (j : n) (s : R) (u : n → R) :
+  det (update_row (s • M) j u) = s ^ (fintype.card n - 1) * det (update_row M j u) :=
+multilinear_map.map_update_smul _ M j s u
+
+lemma det_update_column_smul' (M : matrix n n R) (j : n) (s : R) (u : n → R) :
+  det (update_column (s • M) j u) = s ^ (fintype.card n - 1) * det (update_column M j u) :=
+begin
+  rw [← det_transpose, ← update_row_transpose, transpose_smul, det_update_row_smul'],
+  simp [update_row_transpose, det_transpose]
+end
+
 section det_eq
 
 /-! ### `det_eq` section

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -121,6 +121,10 @@ begin
   { intros j, rw [matrix.one_eq_pi_single, pi.single_comm] }
 end
 
+lemma cramer_smul (r : α) (A : matrix n n α) :
+  cramer (r • A) = r ^ (fintype.card n - 1) • cramer A :=
+linear_map.ext $ λ b, funext $ λ _, det_update_column_smul' _ _ _ _
+
 @[simp] lemma cramer_subsingleton_apply [subsingleton n] (A : matrix n n α) (b : n → α) (i : n) :
   cramer A b i = b i :=
 by rw [cramer_apply, det_eq_elem_of_subsingleton _ i, update_column_self]
@@ -237,6 +241,13 @@ calc adjugate A ⬝ A = (Aᵀ ⬝ (adjugate Aᵀ))ᵀ :
   by rw [←adjugate_transpose, ←transpose_mul, transpose_transpose]
 ... = A.det • 1 : by rw [mul_adjugate (Aᵀ), det_transpose, transpose_smul, transpose_one]
 
+lemma adjugate_smul (r : α) (A : matrix n n α) :
+  adjugate (r • A) = r ^ (fintype.card n - 1) • adjugate A :=
+begin
+  rw [adjugate, adjugate, transpose_smul, cramer_smul],
+  refl,
+end
+
 /-- `det_adjugate_of_cancel` is an auxiliary lemma for computing `(adjugate A).det`,
   used in `det_adjugate_eq_one` and `det_adjugate_of_is_unit`.
 
@@ -606,7 +617,7 @@ begin
   { simp [nonsing_inv_apply_not_is_unit _ h] }
 end
 
-lemma ring_hom.map_adjugate {R S : Type*} [comm_ring R] [comm_ring S] (f : R →+* S)
+lemma _root_.ring_hom.map_adjugate {R S : Type*} [comm_ring R] [comm_ring S] (f : R →+* S)
   (M : matrix n n R) : f.map_matrix M.adjugate = matrix.adjugate (f.map_matrix M) :=
 begin
   ext i k,
@@ -617,6 +628,14 @@ begin
       this, ←map_update_row, ←ring_hom.map_matrix_apply, ←ring_hom.map_det, ←adjugate_apply]
 end
 
+lemma adjugate_conj_transpose [star_ring α] (A : matrix n n α) : A.adjugateᴴ = adjugate (Aᴴ) :=
+begin
+  dsimp only [conj_transpose],
+  have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) :=
+    ((star_ring_aut : α ≃+* α).to_ring_hom.map_adjugate Aᵀ),
+  rw [A.adjugate_transpose, this],
+end
+
 lemma is_regular_of_is_left_regular_det {A : matrix n n α} (hA : is_left_regular A.det) :
   is_regular A :=
 begin

src/linear_algebra/multilinear/basic.lean

@@ -600,6 +600,15 @@ lemma map_smul_univ [fintype ι] (c : ι → R) (m : Πi, M₁ i) :
   f (λi, c i • m i) = (∏ i, c i) • f m :=
 by simpa using map_piecewise_smul f c m finset.univ
 
+@[simp] lemma map_update_smul [fintype ι] (m : Πi, M₁ i) (i : ι) (c : R) (x : M₁ i) :
+  f (update (c • m) i x) = c^(fintype.card ι - 1) • f (update m i x) :=
+begin
+  have : f ((finset.univ.erase i).piecewise (c • update m i x) (update m i x))
+       = (∏ i in finset.univ.erase i, c) • f (update m i x) :=
+    map_piecewise_smul f _ _ _,
+  simpa [←function.update_smul c m] using this,
+end
+
 section distrib_mul_action
 
 variables {R' A : Type*} [monoid R'] [semiring A]