feat: inverse of a 1×1 matrix (#17298)

The statement is a little strange, so it comes with a docstring to justify it.

From https://github.com/eric-wieser/lean-matrix-cookbook



Co-authored-by: Eric Wieser <efw@google.com>

Author: eric-wieser

Mathlib/Data/Matrix/Basic.lean

@@ -492,6 +492,11 @@ theorem diagonal_conjTranspose [AddMonoid α] [StarAddMonoid α] (v : n → α)
   rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
   rfl
 
+theorem diagonal_unique [Unique m] [DecidableEq m] [Zero α] (d : m → α) :
+    diagonal d = of fun _ _ => d default := by
+  ext i j
+  rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
+
 section One
 
 variable [Zero α] [One α]

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -470,6 +470,10 @@ theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A :=
 theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det := by
   rw [Matrix.det_nonsing_inv, isUnit_ring_inverse]
 
+@[simp]
+theorem isUnit_nonsing_inv_iff {A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A := by
+  simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]
+
 -- `IsUnit.invertible` lifts the proposition `IsUnit A` to a constructive inverse of `A`.
 /-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is
 therefore noncomputable. -/
@@ -607,6 +611,24 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse
 
 end Diagonal
 
+/-- The inverse of a 1×1 or 0×0 matrix is always diagonal.
+
+While we could write this as `of fun _ _ => Ring.inverse (A default default)` on the RHS, this is
+less useful because:
+
+* It wouldn't work for 0×0 matrices.
+* More things are true about diagonal matrices than constant matrices, and so more lemmas exist.
+
+`Matrix.diagonal_unique` can be used to reach this form, while `Ring.inverse_eq_inv` can be used
+to replace `Ring.inverse` with `⁻¹`.
+-/
+@[simp]
+theorem inv_subsingleton [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) :
+    A⁻¹ = diagonal fun i => Ring.inverse (A i i) := by
+  rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]
+  congr! with i
+  exact det_eq_elem_of_subsingleton _ _
+
 section Woodbury
 
 variable [Fintype m] [DecidableEq m]