mathlib3

50781196 - feat(data/matrix/block): add `matrix.block_diag` and `matrix.block_diag'` (#13918)

feat(data/matrix/block): add `matrix.block_diag` and `matrix.block_diag'` (#13918) `matrix.block_diag` is to `matrix.block_diagonal` as `matrix.diag` is to `matrix.diagonal`. As well as the basic arithmetic lemmas and bundling, this also adds continuity lemmas. These definitions are primarily an auxiliary construction to prove `matrix.tsum_block_diagonal`, and `matrix.tsum_block_diagonal'`, which are really the main goal of this PR.