Theorems · Definition · linear algebra

Matrix.fromCols

{R : Type u_1} →
  {m : Type u_2} → {n₁ : Type u_6} → {n₂ : Type u_7} → Matrix m n₁ R → Matrix m n₂ R → Matrix m (n₁ ⊕ n₂) R

Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

Defined in

Mathlib.Data.Matrix.ColumnRowPartitioned

Cited by

30 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound