mathlib3

c3c7c349 - feat(data/matrix/basic): dependently-typed block diagonal (#7068)

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.