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_isUpperTriangular and Matrix.det_of_isLowerTriangular: the determinant of a triangular matrix is the product of the entries along the diagonal

Tags #

matrix, diagonal, det, block triangular

source

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

Prop

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 i → M i j = 0

Instances For

source

@[reducible, inline]

abbrev Matrix.IsUpperTriangular {m : Type u_2} {R : Type v} [Zero R] [LT m] (M : Matrix m m R) :

Prop

M is upper triangular: entries below the diagonal vanish.

Equations

M.IsUpperTriangular = M.BlockTriangular id

Instances For

source

@[reducible, inline]

abbrev Matrix.IsLowerTriangular {m : Type u_2} {R : Type v} [Zero R] [LT m] (M : Matrix m m R) :

Prop

M is lower triangular: entries above the diagonal vanish.

Equations

M.IsLowerTriangular = M.BlockTriangular ⇑OrderDual.toDual

Instances For

source

def Matrix.IsIndecomposable {m : Type u_2} {R : Type v} [Zero R] (M : Matrix m m R) :

Prop

A matrix is indecomposable if it cannot be reindexed to block-triangular form.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Matrix.BlockTriangular.submatrix {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [LT α] [Zero R] {f : n → m} (h : M.BlockTriangular b) :

(M.submatrix f f).BlockTriangular (b ∘ f)

source

theorem Matrix.blockTriangular_reindex_iff {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} {M : Matrix m m R} [LT α] [Zero R] {b : n → α} {e : m ≃ n} :

((reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)

source

theorem Matrix.BlockTriangular.transpose {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [LT α] [Zero R] :

M.BlockTriangular b → M.transpose.BlockTriangular (⇑OrderDual.toDual ∘ b)

source

@[simp]

theorem Matrix.blockTriangular_transpose_iff {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} [LT α] [Zero R] {b : m → αᵒᵈ} :

M.transpose.BlockTriangular b ↔ M.BlockTriangular (⇑OrderDual.ofDual ∘ b)

source

@[simp]

theorem Matrix.blockTriangular_zero {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [LT α] [Zero R] :

BlockTriangular 0 b

source

@[instance_reducible]

instance Matrix.decidableBlockTriangular {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [LT α] [Zero R] [DecidableEq R] [Fintype m] [DecidableLT α] :

Decidable (M.BlockTriangular b)

Equations

Matrix.decidableBlockTriangular = decidable_of_iff (∀ (ij : m × m), b ij.2 < b ij.1 → M ij.1 ij.2 = 0) ⋯

source

theorem Matrix.BlockTriangular.neg {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [LT α] [NegZeroClass R] {M : Matrix m m R} (hM : M.BlockTriangular b) :

(-M).BlockTriangular b

source

theorem Matrix.BlockTriangular.add {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [AddZeroClass R] (hM : M.BlockTriangular b) (hN : N.BlockTriangular b) :

(M + N).BlockTriangular b

source

theorem Matrix.BlockTriangular.sub {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [SubNegZeroMonoid R] (hM : M.BlockTriangular b) (hN : N.BlockTriangular b) :

(M - N).BlockTriangular b

source

theorem Matrix.BlockTriangular.add_iff_right {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [AddGroup R] (hM : M.BlockTriangular b) :

(M + N).BlockTriangular b ↔ N.BlockTriangular b

source

theorem Matrix.BlockTriangular.add_iff_left {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [AddGroup R] (hN : N.BlockTriangular b) :

(M + N).BlockTriangular b ↔ M.BlockTriangular b

source

theorem Matrix.BlockTriangular.sub_iff_right {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [AddGroup R] (hM : M.BlockTriangular b) :

(M - N).BlockTriangular b ↔ N.BlockTriangular b

source

theorem Matrix.BlockTriangular.sub_iff_left {α : Type u_1} {m : Type u_2} {R : Type v} {M N : Matrix m m R} {b : m → α} [LT α] [AddGroup R] (hN : N.BlockTriangular b) :

(M - N).BlockTriangular b ↔ M.BlockTriangular b

source

theorem Matrix.BlockTriangular.map {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [LT α] {S : Type u_6} {F : Type u_7} [FunLike F R S] [Zero R] [Zero S] [ZeroHomClass F R S] (f : F) (h : M.BlockTriangular b) :

(M.map ⇑f).BlockTriangular b

source

theorem Matrix.BlockTriangular.comp {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} {b : m → α} [LT α] [Zero R] {M : Matrix m m (Matrix n n R)} (h : M.BlockTriangular b) :

((Matrix.comp m m n n R) M).BlockTriangular fun (i : m × n) => b i.1

source

theorem Matrix.blockTriangular_diagonal {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [Zero R] [DecidableEq m] (d : m → R) :

(diagonal d).BlockTriangular b

source

theorem Matrix.blockTriangular_blockDiagonal' {α : Type u_1} {m' : α → Type u_4} {R : Type v} [Preorder α] [Zero R] [DecidableEq α] (d : (i : α) → Matrix (m' i) (m' i) R) :

(blockDiagonal' d).BlockTriangular Sigma.fst

source

theorem Matrix.blockTriangular_blockDiagonal {α : Type u_1} {m : Type u_2} {R : Type v} [Preorder α] [Zero R] [DecidableEq α] (d : α → Matrix m m R) :

(blockDiagonal d).BlockTriangular Prod.snd

source

theorem Matrix.blockTriangular_one {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [Zero R] [DecidableEq m] [One R] :

BlockTriangular 1 b

source

theorem Matrix.blockTriangular_single {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [Zero R] [DecidableEq m] {i j : m} (hij : b i ≤ b j) (c : R) :

(single i j c).BlockTriangular b

source

theorem Matrix.blockTriangular_single' {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [Zero R] [DecidableEq m] {i j : m} (hij : b j ≤ b i) (c : R) :

(single i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)

source

theorem Matrix.blockTriangular_transvection {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [CommRing R] [DecidableEq m] {i j : m} (hij : b i ≤ b j) (c : R) :

(transvection i j c).BlockTriangular b

source

theorem Matrix.blockTriangular_transvection' {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [Preorder α] [CommRing R] [DecidableEq m] {i j : m} (hij : b j ≤ b i) (c : R) :

(transvection i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)

source

theorem Matrix.BlockTriangular.mul {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [LinearOrder α] [Fintype m] [NonUnitalNonAssocSemiring R] {M N : Matrix m m R} (hM : M.BlockTriangular b) (hN : N.BlockTriangular b) :

(M * N).BlockTriangular b

source

def Matrix.blockTriangularSubsemiring {α : Type u_1} {m : Type u_2} (R : Type v) (b : m → α) [LinearOrder α] [DecidableEq m] [Fintype m] [Semiring R] :

Subsemiring (Matrix m m R)

BlockTriangular matrices form a subsemiring.

Equations

Matrix.blockTriangularSubsemiring R b = { carrier := {M : Matrix m m R | M.BlockTriangular b}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.coe_blockTriangularSubsemiring {α : Type u_1} {m : Type u_2} (R : Type v) (b : m → α) [LinearOrder α] [DecidableEq m] [Fintype m] [Semiring R] :

↑(blockTriangularSubsemiring R b) = {M : Matrix m m R | M.BlockTriangular b}

source

@[simp]

theorem Matrix.mem_blockTriangularSubsemiring {α : Type u_1} {m : Type u_2} {R : Type v} {b : m → α} [LinearOrder α] [DecidableEq m] [Fintype m] [Semiring R] {M : Matrix m m R} :

M ∈ blockTriangularSubsemiring R b ↔ M.BlockTriangular b

source

theorem Matrix.BlockTriangular.pow {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [LinearOrder α] [DecidableEq m] [Fintype m] [Semiring R] (hM : M.BlockTriangular b) (n : ℕ) :

(M ^ n).BlockTriangular b

source

theorem Matrix.blockTriangular_algebraMap {α : Type u_1} {m : Type u_2} {R : Type v} {A : Type u_5} {b : m → α} [LinearOrder α] [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq m] [Fintype m] (r : R) :

((algebraMap R (Matrix m m A)) r).BlockTriangular b

source

def Matrix.blockTriangularSubalgebra {α : Type u_1} {m : Type u_2} (R : Type v) (A : Type u_5) (b : m → α) [LinearOrder α] [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq m] [Fintype m] :

Subalgebra R (Matrix m m A)

BlockTriangular matrices form a subalgebra.

Equations

Matrix.blockTriangularSubalgebra R A b = { toSubsemiring := Matrix.blockTriangularSubsemiring A b, algebraMap_mem' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.mem_blockTriangularSubalgebra {α : Type u_1} {m : Type u_2} {R : Type v} {A : Type u_5} {b : m → α} [LinearOrder α] [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq m] [Fintype m] {M : Matrix m m A} :

M ∈ blockTriangularSubalgebra R A b ↔ M.BlockTriangular b

source

theorem Matrix.isIndecomposable_iff_blockTriangular_const {α : Type u_1} {m : Type u_2} {R : Type v} [LinearOrder α] [Nontrivial α] [Finite m] [Zero R] (M : Matrix m m R) :

M.IsIndecomposable ↔ ∀ (b : m → α), M.BlockTriangular b → ∃ (a : α), b = Function.const m a

source

theorem Matrix.upper_two_blockTriangular {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} [Zero R] [Preorder α] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) {a b : α} (hab : a < b) :

(fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun (x : m) => a) fun (x : n) => b)

Determinant #

source

theorem Matrix.equiv_block_det {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] (M : Matrix m m R) {p q : m → Prop} [DecidablePred p] [DecidablePred q] (e : ∀ (x : m), q x ↔ p x) :

(M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

source

theorem Matrix.det_toSquareBlock_id {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] (M : Matrix m m R) (i : m) :

(M.toSquareBlock id i).det = M i i

source

theorem Matrix.det_toBlock {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] (M : Matrix m m R) (p : m → Prop) [DecidablePred p] :

M.det = (fromBlocks (M.toBlock p p) (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

source

theorem Matrix.twoBlockTriangular_det {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] (M : Matrix m m R) (p : m → Prop) [DecidablePred p] (h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0) :

M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det

source

theorem Matrix.twoBlockTriangular_det' {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] (M : Matrix m m R) (p : m → Prop) [DecidablePred p] (h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0) :

M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det

source

theorem Matrix.BlockTriangular.det {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [DecidableEq α] [LinearOrder α] (hM : M.BlockTriangular b) :

M.det = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).det

source

theorem Matrix.BlockTriangular.det_fintype {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [DecidableEq α] [Fintype α] [LinearOrder α] (h : M.BlockTriangular b) :

M.det = ∏ k : α, (M.toSquareBlock b k).det

source

theorem Matrix.det_of_isUpperTriangular {m : Type u_2} {R : Type v} {M : Matrix m m R} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder m] (h : M.IsUpperTriangular) :

M.det = ∏ i : m, M i i

source

@[deprecated Matrix.det_of_isUpperTriangular (since := "2026-07-30")]

theorem Matrix.det_of_upperTriangular {m : Type u_2} {R : Type v} {M : Matrix m m R} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder m] (h : M.IsUpperTriangular) :

M.det = ∏ i : m, M i i

Alias of Matrix.det_of_isUpperTriangular.

source

theorem Matrix.det_of_isLowerTriangular {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder m] (M : Matrix m m R) (h : M.IsLowerTriangular) :

M.det = ∏ i : m, M i i

source

@[deprecated Matrix.det_of_isLowerTriangular (since := "2026-07-30")]

theorem Matrix.det_of_lowerTriangular {m : Type u_2} {R : Type v} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder m] (M : Matrix m m R) (h : M.IsLowerTriangular) :

M.det = ∏ i : m, M i i

Alias of Matrix.det_of_isLowerTriangular.

source

theorem Matrix.matrixOfPolynomials_blockTriangular {R : Type u_6} [Semiring R] {n : ℕ} (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i) :

(of fun (i j : Fin n) => (p j).coeff ↑i).BlockTriangular id

source

theorem Matrix.det_matrixOfPolynomials {R : Type v} [CommRing R] {n : ℕ} (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i) (h_monic : ∀ (i : Fin n), (p i).Monic) :

(of fun (i j : Fin n) => (p j).coeff ↑i).det = 1

Invertible #

source

theorem Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder α] [Invertible 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

source

theorem Matrix.BlockTriangular.inv_toBlock {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder α] [Invertible 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⁻¹.

source

@[instance_reducible]

def Matrix.BlockTriangular.invertibleToBlock {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder α] [Invertible 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

hM.invertibleToBlock k = invertibleOfLeftInverse (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) ⋯

Instances For

source

theorem Matrix.toBlock_inverse_eq_zero {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder α] [Invertible 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.

source

theorem Matrix.blockTriangular_inv_of_blockTriangular {α : Type u_1} {m : Type u_2} {R : Type v} {M : Matrix m m R} {b : m → α} [CommRing R] [DecidableEq m] [Fintype m] [LinearOrder α] [Invertible M] (hM : M.BlockTriangular b) :

M⁻¹.BlockTriangular b

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

Documentation

Mathlib.LinearAlgebra.Matrix.Block

Block matrices and their determinant #

Main definitions #

Main results #

Tags #

Determinant #

Invertible #