mathlib3

3e6e34e4 - feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767)

feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767) Notably this includes the proof of the determinant of a block matrix, which we didn't seem to have in the general case. This also renames some of the lemmas about determinants of block matrices, and adds some missing API for `inv_of` on matrices. There's some discussion at https://math.stackexchange.com/q/4105846/1896 about whether this name is appropriate, and whether it should be called "Sylvester's determinant theorem" instead.