Stacking matrices

Stream: Is there code for X?

[Alexander Bentkamp]

Is there code to stack matrices next to each other or above each other like this:

def hcompose (A : matrix m n R) (B : matrix m k R) : matrix m (n ⊕ k) R :=
λ i j, sum.cases_on j (λ j, A i j) (λ j, B i j)

def vcompose (A : matrix m n R) (B : matrix k n R) : matrix (m ⊕ k) n R :=
λ i j, sum.cases_on i (λ i, A i j) (λ i, B i j)

[Eric Wieser]

This came up recently at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Concatenate.20matrices/near/279417465

[Eric Wieser]

Note that hcompose is "just" sum.elim:

def vcompose (A : matrix m n R) (B : matrix k n R) : matrix (m ⊕ k) n R :=
sum.elim A B

(although wrapping it in a deinition makes it type-correct, vs using sum.elim directly which forgets the matrix-ness)

[Eric Wieser]

hcompose you can golf either with

def hcompose (A : matrix m n R) (B : matrix m k R) : matrix m (n ⊕ k) R :=
λ i, sum.elim (A i) (B i)

or

def hcompose (A : matrix m n R) (B : matrix m k R) : matrix m (n ⊕ k) R :=
(sum.elim Aᵀ Bᵀ)ᵀ

[Alexander Bentkamp]

Thanks!