Commit 2022-05-05 02:21 50781196
View on Github →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.