mathlib3

3d58fce5 - feat(linear_algebra): determinant of `matrix.block_diagonal` (#4300)

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.