Theorems · Definition · linear algebra

Matrix.BlockTriangular

{α : Type u_1} → {m : Type u_3} → {R : Type v} → [LT α] → [Zero R] → Matrix m m R → (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.

Defined in

Mathlib.LinearAlgebra.Matrix.Block

Cited by

45 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

LTZero