invertibleOfFromBlocksZero₂₁Invertible

English

If a block matrix is invertible, then both diagonal blocks are invertible (reading off the diagonal of the inverse).

Русский

Если блочная матрица обратима, то обе диагональные части обратимы (по диагонали обратной матрицы).

LaTeX

$$$\text{Invertible}(\mathrm{fromBlocks}(A,B,0,D)) \Rightarrow (\text{Invertible}(A) \land \text{Invertible}(D))$$$

Lean4

/-- Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading
off the diagonal entries of the inverse). -/
def invertibleOfFromBlocksZero₂₁Invertible (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α)
    [Invertible (fromBlocks A B 0 D)] : Invertible A × Invertible D
    where
  fst :=
    invertibleOfLeftInverse _ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ <|
      by
      have := invOf_mul_self (fromBlocks A B 0 D)
      rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
      replace := congr_arg Matrix.toBlocks₁₁ this
      simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.mul_zero, add_zero, ← fromBlocks_one] using this
  snd :=
    invertibleOfRightInverse _ (⅟(fromBlocks A B 0 D)).toBlocks₂₂ <|
      by
      have := mul_invOf_self (fromBlocks A B 0 D)
      rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
      replace := congr_arg Matrix.toBlocks₂₂ this
      simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.zero_mul, zero_add, ← fromBlocks_one] using this

Похожие утверждения