English
If the matrix is defined on a singleton (0×0 or 1×1) index set, its inverse is diagonal with diagonal entries given by the ring inverse of the corresponding entries.
Русский
Если матрица имеет размер 1×1 или 0×0, её обратная диагональная матрица имеет диагональные элементы, равные обратным соответствующих элементов (по кольцу).
LaTeX
$$A⁻¹ = diagonal( Ring.inverse(A_{ii}) ) for subsingleton indices$$
Lean4
/-- 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 _ _
