feat(linear_algebra/matrix/nonsingular_inverse): interchange of matri…

…x reindexing and inversion (#18812)

This follows the strategy taken in #13827, which gives us all of:

* `is_unit (A.submatrix e₁ e₂) ↔ is_unit A`
* `(A.submatrix e₁ e₂)⁻¹ = (A⁻¹).submatrix e₂ e₁`
* `⅟(A.submatrix e₁ e₂) = (⅟A).submatrix e₂ e₁`
* `invertible (A.submatrix e₁ e₂) ≃ invertible A`

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -451,6 +451,8 @@ begin
   rw [smul_mul, mul_adjugate, units.smul_def, smul_smul, h.coe_inv_mul, one_smul]
 end
 
+section diagonal
+
 /-- `diagonal v` is invertible if `v` is -/
 def diagonal_invertible {α} [non_assoc_semiring α] (v : n → α) [invertible v] :
   invertible (diagonal v) :=
@@ -508,6 +510,8 @@ begin
     rw [ring.inverse_non_unit _ h, pi.zero_def, diagonal_zero, ring.inverse_non_unit _ this] }
 end
 
+end diagonal
+
 @[simp] lemma inv_inv_inv (A : matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ :=
 begin
   by_cases h : is_unit A.det,
@@ -543,6 +547,74 @@ end
 by rw [← (A⁻¹).transpose_transpose, vec_mul_transpose, transpose_nonsing_inv, ← det_transpose,
     Aᵀ.det_smul_inv_mul_vec_eq_cramer _ (is_unit_det_transpose A h)]
 
+/-! ### Inverses of permutated matrices
+
+Note that the simp-normal form of `matrix.reindex` is `matrix.submatrix`, so we prove most of these
+results about only the latter.
+-/
+
+section submatrix
+variables [fintype m]
+variables [decidable_eq m]
+
+/-- `A.submatrix e₁ e₂` is invertible if `A` is -/
+def submatrix_equiv_invertible (A : matrix m m α) (e₁ e₂ : n ≃ m) [invertible A] :
+  invertible (A.submatrix e₁ e₂) :=
+invertible_of_right_inverse _ ((⅟A).submatrix e₂ e₁) $
+  by rw [matrix.submatrix_mul_equiv, matrix.mul_inv_of_self, submatrix_one_equiv]
+
+/-- `A` is invertible if `A.submatrix e₁ e₂` is -/
+def invertible_of_submatrix_equiv_invertible (A : matrix m m α) (e₁ e₂ : n ≃ m)
+  [invertible (A.submatrix e₁ e₂)] : invertible A :=
+invertible_of_right_inverse _ ((⅟(A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) $ begin
+  have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp,
+  conv in (_ ⬝ _) { congr, rw this },
+  rw [matrix.submatrix_mul_equiv, matrix.mul_inv_of_self, submatrix_one_equiv]
+end
+
+lemma inv_of_submatrix_equiv_eq (A : matrix m m α) (e₁ e₂ : n ≃ m)
+  [invertible A] [invertible (A.submatrix e₁ e₂)] :
+  ⅟(A.submatrix e₁ e₂) = (⅟A).submatrix e₂ e₁ :=
+begin
+  letI := submatrix_equiv_invertible A e₁ e₂,
+  haveI := invertible.subsingleton (A.submatrix e₁ e₂),
+  convert (rfl : ⅟(A.submatrix e₁ e₂) = _),
+end
+
+/-- Together `matrix.submatrix_equiv_invertible` and
+`matrix.invertible_of_submatrix_equiv_invertible` form an equivalence, although both sides of the
+equiv are subsingleton anyway. -/
+@[simps]
+def submatrix_equiv_invertible_equiv_invertible (A : matrix m m α) (e₁ e₂ : n ≃ m) :
+  invertible (A.submatrix e₁ e₂) ≃ invertible A :=
+{ to_fun := λ _, by exactI invertible_of_submatrix_equiv_invertible A e₁ e₂,
+  inv_fun := λ _, by exactI submatrix_equiv_invertible A e₁ e₂,
+  left_inv := λ _, subsingleton.elim _ _,
+  right_inv := λ _, subsingleton.elim _ _ }
+
+/-- When lowered to a prop, `matrix.invertible_of_submatrix_equiv_invertible` forms an `iff`. -/
+@[simp] lemma is_unit_submatrix_equiv {A : matrix m m α} (e₁ e₂ : n ≃ m) :
+  is_unit (A.submatrix e₁ e₂) ↔ is_unit A :=
+by simp only [← nonempty_invertible_iff_is_unit,
+  (submatrix_equiv_invertible_equiv_invertible A _ _).nonempty_congr]
+
+@[simp] lemma inv_submatrix_equiv (A : matrix m m α) (e₁ e₂ : n ≃ m) :
+  (A.submatrix e₁ e₂)⁻¹ = (A⁻¹).submatrix e₂ e₁ :=
+begin
+  by_cases h : is_unit A,
+  { casesI h.nonempty_invertible,
+    letI := submatrix_equiv_invertible A e₁ e₂,
+    rw [←inv_of_eq_nonsing_inv, ←inv_of_eq_nonsing_inv, inv_of_submatrix_equiv_eq] },
+  { have := (is_unit_submatrix_equiv e₁ e₂).not.mpr h,
+    simp_rw [nonsing_inv_eq_ring_inverse, ring.inverse_non_unit _ h, ring.inverse_non_unit _ this,
+      submatrix_zero, pi.zero_apply] }
+end
+
+lemma inv_reindex (e₁ e₂ : n ≃ m) (A : matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ (A⁻¹) :=
+inv_submatrix_equiv A e₁.symm e₂.symm
+
+end submatrix
+
 /-! ### More results about determinants -/
 
 section det