inv_toBlock — Mathlib

English

Under the same setup, an explicit block-equation shows the product of the blockwise inverses equals the identity.

Русский

В той же конфигурации явное блочно-уровневое тождество показывает, что произведение блочно-обратных равно единице.

LaTeX

$$$\big(M^{-1}_{pp}\,M_{pp}\big) \cdot 1 + \cdots = I$$$

Lean4

/-- The inverse of an upper-left subblock of a block-triangular matrix `M` is the upper-left
subblock of `M⁻¹`. -/
theorem inv_toBlock [LinearOrder α] [Invertible M] (hM : BlockTriangular M b) (k : α) :
    (M.toBlock (fun i => b i < k) fun i => b i < k)⁻¹ = M⁻¹.toBlock (fun i => b i < k) fun i => b i < k :=
  inv_eq_left_inv <| hM.toBlock_inverse_mul_toBlock_eq_one k

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