search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 297 forks source link

[Merged by Bors] - feat(linear_algebra/matrix/schur_complement): invertibility of block matrices #19156

Closed eric-wieser closed 1 year ago

eric-wieser commented 1 year ago

Open in Gitpod

Creating this for the purpose of having an easy diff against #18849

mathlib-dependent-issues-bot commented 1 year ago

This PR/issue depends on:

semorrison commented 1 year ago

bors merge

bors[bot] commented 1 year ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.