Theorems · Definition · linear algebra

Matrix.BlockTriangular.invertibleToBlock

{α : Type u_1} →
  {m : Type u_3} →
    {R : Type v} →
      {M : Matrix m m R} →
        {b : m → α} →
          [inst : CommRing R] →
            [inst_1 : DecidableEq m] →
              [inst_2 : Fintype m] →
                [inst_3 : LinearOrder α] →
                  [Invertible M] →
                    M.BlockTriangular b → (k : α) → Invertible (M.toBlock (fun i => b i < k) fun i => b i < k)

An upper-left subblock of an invertible block-triangular matrix is invertible.

Defined in

Mathlib.LinearAlgebra.Matrix.Block

Cited by

2 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingDecidableEqFintypeLinearOrderInvertible