mathlib3

68ead6e6 - feat(linear_algebra/matrix): Schur complement (#15270)

feat(linear_algebra/matrix): Schur complement (#15270) If a matrix `A` is positive definite, then `[A B; Bᴴ D]` is postive semidefinite if and only if `D - Bᴴ A⁻¹ B` is postive semidefinite.