Theorems · Definition · linear algebra

Matrix.fromRows

{R : Type u_1} →
  {m₁ : Type u_3} → {m₂ : Type u_4} → {n : Type u_5} → Matrix m₁ n R → Matrix m₂ n R → Matrix (m₁ ⊕ m₂) n R

Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]

Defined in

Mathlib.Data.Matrix.ColumnRowPartitioned

Cited by

35 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound