# 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.

Equations
• M.BlockTriangular b = ∀ ⦃i j : m⦄, b j < b iM i j = 0
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 : M.BlockTriangular b) :
(M.submatrix f f).BlockTriangular (b f)
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} :
(() M).BlockTriangular b M.BlockTriangular (b e)
theorem Matrix.BlockTriangular.transpose {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [LT α] :
M.BlockTriangular bM.transpose.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αᵒᵈ} :
M.transpose.BlockTriangular b M.BlockTriangular (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 : M.BlockTriangular b) :
(-M).BlockTriangular b
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 : M.BlockTriangular b) (hN : N.BlockTriangular b) :
(M + N).BlockTriangular b
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 : M.BlockTriangular b) (hN : N.BlockTriangular b) :
(M - N).BlockTriangular b
theorem Matrix.blockTriangular_diagonal {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] (d : mR) :
().BlockTriangular b
theorem Matrix.blockTriangular_blockDiagonal' {α : Type u_1} {m' : αType u_6} {R : Type v} [] [] [] (d : (i : α) → Matrix (m' i) (m' i) R) :
.BlockTriangular Sigma.fst
theorem Matrix.blockTriangular_blockDiagonal {α : Type u_1} {m : Type u_3} {R : Type v} [] [] [] (d : αMatrix m m R) :
.BlockTriangular Prod.snd
theorem Matrix.blockTriangular_one {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] :
theorem Matrix.blockTriangular_stdBasisMatrix {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] {i : m} {j : m} (hij : b i b j) (c : R) :
().BlockTriangular b
theorem Matrix.blockTriangular_stdBasisMatrix' {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] {i : m} {j : m} (hij : b j b i) (c : R) :
().BlockTriangular (OrderDual.toDual b)
theorem Matrix.blockTriangular_transvection {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] {i : m} {j : m} (hij : b i b j) (c : R) :
().BlockTriangular b
theorem Matrix.blockTriangular_transvection' {α : Type u_1} {m : Type u_3} {R : Type v} [] {b : mα} [] [] {i : m} {j : m} (hij : b j b i) (c : R) :
().BlockTriangular (OrderDual.toDual b)
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 : M.BlockTriangular b) (hN : N.BlockTriangular b) :
(M * N).BlockTriangular b
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) :
(A.fromBlocks B 0 D).BlockTriangular (Sum.elim (fun (x : m) => a) fun (x : n) => 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) :
(M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det
@[simp]
theorem Matrix.det_toSquareBlock_id {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (i : m) :
(M.toSquareBlock id i).det = M i i
theorem Matrix.det_toBlock {m : Type u_3} {R : Type v} [] [] [] (M : Matrix m m R) (p : mProp) [] :
M.det = ((M.toBlock p p).fromBlocks (M.toBlock p fun (j : m) => ¬p j) (M.toBlock (fun (j : m) => ¬p j) p) (M.toBlock (fun (j : m) => ¬p j) fun (j : m) => ¬p j)).det
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) :
M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det
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) :
M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det
theorem Matrix.BlockTriangular.det {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] (hM : M.BlockTriangular b) :
M.det = (Finset.image b Finset.univ).prod fun (a : α) => (M.toSquareBlock b a).det
theorem Matrix.BlockTriangular.det_fintype {α : Type u_1} {m : Type u_3} {R : Type v} [] {M : Matrix m m R} {b : mα} [] [] [] [] [] (h : M.BlockTriangular b) :
M.det = Finset.univ.prod fun (k : α) => (M.toSquareBlock b k).det
theorem Matrix.det_of_upperTriangular {m : Type u_3} {R : Type v} [] {M : Matrix m m R} [] [] [] (h : M.BlockTriangular id) :
M.det = Finset.univ.prod fun (i : m) => M i i
theorem Matrix.det_of_lowerTriangular {m : Type u_3} {R : Type v} [] [] [] [] (M : Matrix m m R) (h : M.BlockTriangular OrderDual.toDual) :
M.det = Finset.univ.prod fun (i : m) => M i i
theorem Matrix.matrixOfPolynomials_blockTriangular {R : Type v} [] {n : } (p : Fin n) (h_deg : ∀ (i : Fin n), (p i).natDegree i) :
(Matrix.of fun (i j : Fin n) => (p j).coeff i).BlockTriangular id
theorem Matrix.det_matrixOfPolynomials {R : Type v} [] {n : } (p : Fin n) (h_deg : ∀ (i : Fin n), (p i).natDegree = i) (h_monic : ∀ (i : Fin n), (p i).Monic) :
(Matrix.of fun (i j : Fin n) => (p j).coeff i).det = 1

### 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 : M.BlockTriangular b) (k : α) :
((M⁻¹.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k) * M.toBlock (fun (i : m) => b i < k) fun (i : m) => 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 : M.BlockTriangular b) (k : α) :
(M.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k)⁻¹ = M⁻¹.toBlock (fun (i : m) => b i < k) fun (i : m) => 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 : M.BlockTriangular b) (k : α) :
Invertible (M.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k)

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

Equations
• One or more equations did not get rendered due to their size.
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 : M.BlockTriangular b) (k : α) :
(M⁻¹.toBlock (fun (i : m) => k b i) fun (i : m) => 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 : M.BlockTriangular b) :
M⁻¹.BlockTriangular b

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