English
Let A be a matrix; if the scalar inverse map is continuous at det(A), then the matrix inverse map is continuous at A; i.e., A ↦ A^{-1} varies continuously if inverse on scalars is continuous at det(A).
Русский
Пусть A — матрица; если отображение обратного на скалярах непрерывно в точке det(A), то отображение A ↦ A^{-1} непрерывно в точке A.
LaTeX
$$$\\operatorname{ContinuousAt}(\\operatorname{Ring.inverse}, A_{\\det}) \\Rightarrow \\operatorname{ContinuousAt}(\\operatorname{Inv.inv}, A)$$$
Lean4
/-- When `Ring.inverse` is continuous at the determinant (such as in a `NormedRing`, or a
topological field), so is `Matrix.inv`. -/
theorem continuousAt_matrix_inv [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] (A : Matrix n n R)
(h : ContinuousAt Ring.inverse A.det) : ContinuousAt Inv.inv A :=
(h.comp continuous_id.matrix_det.continuousAt).smul continuous_id.matrix_adjugate.continuousAt
