Commit 2020-10-01 14:28 3d58fce5

feat(linear_algebra): determinant of matrix.block_diagonal (#4300) This PR shows the determinant of matrix.block_diagonal is the product of the determinant of each subblock. The only contributing permutations in the expansion of the determinant are those which map each block to the same block. Each of those permutations has the form equiv.prod_congr_left σ. Using equiv.perm.extend and equiv.prod_congr_right, we can compute the sign of equiv.prod_congr_left σ, and with a bit of algebraic manipulation we reach the conclusion.