# Documentation

Mathlib.LinearAlgebra.Matrix.Block

# Block matrices and their determinant #

This file defines a predicate Matrix.BlockTriangular saying a matrix is block triangular, and proves the value of the determinant for various matrices built out of blocks.

## Main definitions #

• Matrix.BlockTriangular expresses that an o by o matrix is block triangular, if the rows and columns are ordered according to some order b : o → α

## Main results #

• Matrix.det_of_blockTriangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocks
• Matrix.det_of_upperTriangular and matrix.det_of_lowerTriangular: the determinant of a triangular matrix is the product of the entries along the diagonal

## Tags #

matrix, diagonal, det, block triangular

def Matrix.BlockTriangular {α : Type u_1} {m : Type u_3} {R : Type v} [] [LT α] (M : Matrix m m R) (b : mα) :

Let b map rows and columns of a square matrix M to blocks indexed by αs. Then BlockTriangular M n b says the matrix is block triangular.

Instances For
@[simp]
theorem Matrix.BlockTriangular.submatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [] {M : Matrix m m R} {b : mα} [LT α] {f : nm} (h : ) :
theorem Matrix.blockTriangular_reindex_iff {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [] {M : Matrix m m R} [LT α] {b : nα} {e : m n} :
theorem Matrix.BlockTriangular.transpose {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [LT α] :
Matrix.BlockTriangular () (OrderDual.toDual b)
@[simp]
theorem Matrix.blockTriangular_transpose_iff {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} [LT α] {b : mαᵒᵈ} :
Matrix.BlockTriangular M (OrderDual.ofDual b)
@[simp]
theorem Matrix.blockTriangular_zero {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [LT α] :
theorem Matrix.BlockTriangular.neg {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [LT α] (hM : ) :
theorem Matrix.BlockTriangular.add {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {N : Matrix m m R} {b : mα} [LT α] (hM : ) (hN : ) :
theorem Matrix.BlockTriangular.sub {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {N : Matrix m m R} {b : mα} [LT α] (hM : ) (hN : ) :
theorem Matrix.blockTriangular_diagonal {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] (d : mR) :
theorem Matrix.blockTriangular_blockDiagonal' {α : Type u_1} {m' : αType u_6} {R : Type v} [] [] [] (d : (i : α) → Matrix (m' i) (m' i) R) :
theorem Matrix.blockTriangular_blockDiagonal {α : Type u_1} {m : Type u_3} {R : Type v} [] [] [] (d : αMatrix m m R) :
theorem Matrix.BlockTriangular.mul {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] {M : Matrix m m R} {N : Matrix m m R} (hM : ) (hN : ) :
theorem Matrix.upper_two_blockTriangular {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [] [] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) {a : α} {b : α} (hab : a < b) :
Matrix.BlockTriangular () (Sum.elim (fun x => a) fun x => b)

### Determinant #

theorem Matrix.equiv_block_det {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) {p : mProp} {q : mProp} [] [] (e : ∀ (x : m), q x p x) :
@[simp]
theorem Matrix.det_toSquareBlock_id {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (i : m) :
Matrix.det () = M i i
theorem Matrix.det_toBlock {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (p : mProp) [] :
= Matrix.det (Matrix.fromBlocks () (Matrix.toBlock M p fun j => ¬p j) (Matrix.toBlock M (fun j => ¬p j) p) (Matrix.toBlock M (fun j => ¬p j) fun j => ¬p j))
theorem Matrix.twoBlockTriangular_det {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (p : mProp) [] (h : ∀ (i : m), ¬p i∀ (j : m), p jM i j = 0) :
theorem Matrix.twoBlockTriangular_det' {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (p : mProp) [] (h : ∀ (i : m), p i∀ (j : m), ¬p jM i j = 0) :
theorem Matrix.BlockTriangular.det {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) :
= Finset.prod (Finset.image b Finset.univ) fun a => Matrix.det ()
theorem Matrix.BlockTriangular.det_fintype {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] [] (h : ) :
= Finset.prod Finset.univ fun k => Matrix.det ()
theorem Matrix.det_of_upperTriangular {m : Type u_3} {R : Type v} [] {M : Matrix m m R} [] [] [] (h : ) :
= Finset.prod Finset.univ fun i => M i i
theorem Matrix.det_of_lowerTriangular {m : Type u_3} {R : Type v} [] [] [] [] (M : Matrix m m R) (h : Matrix.BlockTriangular M OrderDual.toDual) :
= Finset.prod Finset.univ fun i => M i i

### Invertible #

theorem Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) (k : α) :
((Matrix.toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) * Matrix.toBlock M (fun i => b i < k) fun i => b i < k) = 1
theorem Matrix.BlockTriangular.inv_toBlock {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) (k : α) :
(Matrix.toBlock M (fun i => b i < k) fun i => b i < k)⁻¹ = Matrix.toBlock M⁻¹ (fun i => b i < k) fun i => b i < k

The inverse of an upper-left subblock of a block-triangular matrix M is the upper-left subblock of M⁻¹.

def Matrix.BlockTriangular.invertibleToBlock {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) (k : α) :
Invertible (Matrix.toBlock M (fun i => b i < k) fun i => b i < k)

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

Instances For
theorem Matrix.toBlock_inverse_eq_zero {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) (k : α) :
(Matrix.toBlock M⁻¹ (fun i => k b i) fun i => b i < k) = 0

A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step towards BlockTriangular.inv_toBlock below.

theorem Matrix.blockTriangular_inv_of_blockTriangular {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : ) :

The inverse of a block-triangular matrix is block-triangular.