# mathlib3documentation

linear_algebra.matrix.block

# Block matrices and their determinant #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• matrix.block_triangular expresses that a 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_block_triangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocks
• matrix.det_of_upper_triangular and matrix.det_of_lower_triangular: the determinant of a triangular matrix is the product of the entries along the diagonal

## Tags #

matrix, diagonal, det, block triangular

def matrix.block_triangular {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] [has_lt α] (M : m R) (b : m α) :
Prop

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

Equations
• = ⦃i j : m⦄, b j < b i M i j = 0
@[protected, simp]
theorem matrix.block_triangular.submatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [comm_ring R] {M : m R} {b : m α} [has_lt α] {f : n m} (h : M.block_triangular b) :
theorem matrix.block_triangular_reindex_iff {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [comm_ring R] {M : m R} [has_lt α] {b : n α} {e : m n} :
@[protected]
theorem matrix.block_triangular.transpose {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [has_lt α] :
@[protected, simp]
theorem matrix.block_triangular_transpose_iff {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} [has_lt α] {b : m αᵒᵈ} :
@[simp]
theorem matrix.block_triangular_zero {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {b : m α} [has_lt α] :
@[protected]
theorem matrix.block_triangular.neg {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [has_lt α] (hM : M.block_triangular b) :
theorem matrix.block_triangular.add {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M N : m R} {b : m α} [has_lt α] (hM : M.block_triangular b) (hN : N.block_triangular b) :
theorem matrix.block_triangular.sub {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M N : m R} {b : m α} [has_lt α] (hM : M.block_triangular b) (hN : N.block_triangular b) :
theorem matrix.block_triangular_diagonal {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {b : m α} [preorder α] [decidable_eq m] (d : m R) :
theorem matrix.block_triangular_block_diagonal' {α : Type u_1} {m' : α Type u_6} {R : Type v} [comm_ring R] [preorder α] [decidable_eq α] (d : Π (i : α), matrix (m' i) (m' i) R) :
theorem matrix.block_triangular_block_diagonal {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] [preorder α] [decidable_eq α] (d : α m R) :
theorem matrix.block_triangular.mul {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {b : m α} [linear_order α] [fintype m] {M N : m R} (hM : M.block_triangular b) (hN : N.block_triangular b) :
theorem matrix.upper_two_block_triangular {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [comm_ring R] [preorder α] (A : m R) (B : n R) (D : n R) {a b : α} (hab : a < b) :
0 D).block_triangular (sum.elim (λ (i : m), a) (λ (j : n), b))

### Determinant #

theorem matrix.equiv_block_det {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : m R) {p q : m Prop} (e : (x : m), q x p x) :
@[simp]
theorem matrix.det_to_square_block_id {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : m R) (i : m) :
i).det = M i i
theorem matrix.det_to_block {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : m R) (p : m Prop)  :
M.det = (matrix.from_blocks (M.to_block p p) (M.to_block p (λ (j : m), ¬p j)) (M.to_block (λ (j : m), ¬p j) p) (M.to_block (λ (j : m), ¬p j) (λ (j : m), ¬p j))).det
theorem matrix.two_block_triangular_det {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : m R) (p : m Prop) (h : (i : m), ¬p i (j : m), p j M i j = 0) :
M.det = (M.to_square_block_prop p).det * (M.to_square_block_prop (λ (i : m), ¬p i)).det
theorem matrix.two_block_triangular_det' {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : m R) (p : m Prop) (h : (i : m), p i (j : m), ¬p j M i j = 0) :
M.det = (M.to_square_block_prop p).det * (M.to_square_block_prop (λ (i : m), ¬p i)).det
@[protected]
theorem matrix.block_triangular.det {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [decidable_eq α] [linear_order α] (hM : M.block_triangular b) :
M.det = (λ (a : α), (M.to_square_block b a).det)
theorem matrix.block_triangular.det_fintype {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [decidable_eq α] [fintype α] [linear_order α] (h : M.block_triangular b) :
M.det = finset.univ.prod (λ (k : α), (M.to_square_block b k).det)
theorem matrix.det_of_upper_triangular {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} [decidable_eq m] [fintype m] [linear_order m] (h : M.block_triangular id) :
M.det = finset.univ.prod (λ (i : m), M i i)
theorem matrix.det_of_lower_triangular {m : Type u_3} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] [linear_order m] (M : m R)  :
M.det = finset.univ.prod (λ (i : m), M i i)

### Invertible #

theorem matrix.block_triangular.to_block_inverse_mul_to_block_eq_one {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [linear_order α] [invertible M] (hM : M.block_triangular b) (k : α) :
(M⁻¹.to_block (λ (i : m), b i < k) (λ (i : m), b i < k)).mul (M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k)) = 1
theorem matrix.block_triangular.inv_to_block {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [linear_order α] [invertible M] (hM : M.block_triangular b) (k : α) :
(M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k))⁻¹ = M⁻¹.to_block (λ (i : m), b i < k) (λ (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.block_triangular.invertible_to_block {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [linear_order α] [invertible M] (hM : M.block_triangular b) (k : α) :
invertible (M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k))

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

Equations
theorem matrix.to_block_inverse_eq_zero {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [linear_order α] [invertible M] (hM : M.block_triangular b) (k : α) :
M⁻¹.to_block (λ (i : m), k b i) (λ (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 block_triangular.inv_to_block below.

theorem matrix.block_triangular_inv_of_block_triangular {α : Type u_1} {m : Type u_3} {R : Type v} [comm_ring R] {M : m R} {b : m α} [decidable_eq m] [fintype m] [linear_order α] [invertible M] (hM : M.block_triangular b) :

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