Theorems · Definition · linear algebra

Matrix.fromBlocks

{l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {o : Type u_4} →
        {α : Type u_12} → Matrix n l α → Matrix n m α → Matrix o l α → Matrix o m α → Matrix (n ⊕ o) (l ⊕ m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Defined in

Mathlib.Data.Matrix.Block

Cited by

108 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 64 definitions · uses Quot.sound