invertibleToBlock — Mathlib

English

For a block-triangular M, the lower-left block of its inverse is zero when considering the corresponding index partition.

Русский

Для блочно-верхнетреугольной M нижний левый блок её обратной матрицы равен нулю в соответствующем разбиении индексов.

LaTeX

$$$\big(M^{-1}\big)_{\lnot p p} = 0$$$

Lean4

/-- An upper-left subblock of an invertible block-triangular matrix is invertible. -/
def invertibleToBlock [LinearOrder α] [Invertible M] (hM : BlockTriangular M b) (k : α) :
    Invertible (M.toBlock (fun i => b i < k) fun i => b i < k) :=
  invertibleOfLeftInverse _ ((⅟M).toBlock (fun i => b i < k) fun i => b i < k) <| by
    simpa only [invOf_eq_nonsing_inv] using hM.toBlock_inverse_mul_toBlock_eq_one k

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