English
Suppose IsUnit A ⇔ IsUnit D. Then, if both (A - B ⅟D C) and fromBlocks A B C D are invertible, the inverse of the block matrix is given by the explicit block formula with D and A inverted accordingly.
Русский
Пусть IsUnit A ⇔ IsUnit D. Тогда при обратимости (A - B D^{-1} C) и fromBlocks A B C D обратная матрица имеет блочное представление.
LaTeX
$$$\text{IsUnit}(A) \iff \text{IsUnit}(D) \Rightarrow \bigl(\mathrm{fromBlocks}(A,B,C,D)\bigr)^{-1} = \mathrm{fromBlocks}(A^{-1}, -(A^{-1} B D^{-1}), -(D^{-1} C A^{-1}), D^{-1} )$$$
Lean4
/-- An expression for the inverse of an upper block-triangular matrix, when either both elements of
diagonal are invertible, or both are not. -/
theorem inv_fromBlocks_zero₂₁_of_isUnit_iff (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α)
(hAD : IsUnit A ↔ IsUnit D) : (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹ :=
by
by_cases hA : IsUnit A
· have hD := hAD.mp hA
cases hA.nonempty_invertible
cases hD.nonempty_invertible
letI := fromBlocksZero₂₁Invertible A B D
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₂₁_eq]
· have hD := hAD.not.mp hA
have : ¬IsUnit (fromBlocks A B 0 D) := isUnit_fromBlocks_zero₂₁.not.mpr (not_and'.mpr fun _ => hA)
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]
