Commit 2020-09-26 07:58 18927246

feat(data/matrix): definition of block_diagonal (#4257) This PR defines matrix.block_diagonal : (o -> matrix m n R) -> matrix (m × o) (n × o) R. The choice to put o on the right hand side of the product will help with relating this to is_basis.smul, but it won't be a huge hassle to write matrix (o × m) (o × m) R instead if you prefer. I also tried making m and n depend on o, giving block_diagonal M : matrix (Σ k : o, m k) (Σ k : o, n k) R, but that turned out to be a shotcut to eq.rec hell.