English
Symmetric to the₂₂ case: if IsUnit A ⇔ IsUnit D, then the inverse of fromBlocks A 0 C D is given by a block expression with A^{-1} and D^{-1}.
Русский
Симметрично к случаю ₂₂: если IsUnit A ⇔ IsUnit D, то обратная матрица fromBlocks A 0 C D имеет блочное представление с A^{-1} и D^{-1}.
LaTeX
$$$\text{IsUnit}(A) \iff \text{IsUnit}(D) \Rightarrow ⅟(\mathrm{fromBlocks}(A,0,C,D)) = \mathrm{fromBlocks}(A^{-1}, 0, -(D^{-1} C A^{-1}), D^{-1})$$$
Lean4
/-- An expression for the inverse of a lower 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 α) (C : Matrix n m α) (D : Matrix n n α)
(hAD : IsUnit A ↔ IsUnit D) : (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹ :=
by
by_cases hA : IsUnit A
· have hD := hAD.mp hA
cases hA.nonempty_invertible
cases hD.nonempty_invertible
letI := fromBlocksZero₁₂Invertible A C D
simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₁₂_eq]
· have hD := hAD.not.mp hA
have : ¬IsUnit (fromBlocks A 0 C 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]
