Commit 2021-04-07 15:23 c3c7c349

feat(data/matrix/basic): dependently-typed block diagonal (#7068) This allows constructing block diagonal matrices whose blocks are different sizes. A notable example of such a matrix is the one from the Jordan Normal Form. This duplicates all of the API for block_diagonal from this file. Most of the proofs copy across cleanly, but the proof for block_diagonal_mul' required lots of hand-holding that simp could solve by itself for the non-dependent case.