Theorems · Definition · linear algebra

Matrix.toSquareBlock

{m : Type u_2} →
  {α : Type u_12} → {β : Type u_13} → Matrix m m α → (b : m → β) → (k : β) → Matrix { a // b a = k } { a // b a = k } α

Let b map rows and columns of a square matrix M to blocks. Then toSquareBlock M b k is the block k matrix.

Defined in

Mathlib.Data.Matrix.Block

Cited by

15 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound