-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(linear_algebra/matrix/schur_complement): invertibility of block matrices #19156
Conversation
…ck matrices with an invertible corner
… matrices are invertible iff their diagonal is This follows the pattern used for `submatrix` and `diagonal` of setting up ```lean invertible (from_blocks A B 0 D) ≃ invertible A × invertible D ``` and using it to prove ```lean is_unit (from_blocks A B 0 D) ↔ is_unit A ∧ is_unit D ``` These results fall out as the special case of the general formula; though my hope is that they can also be used to prove it.
… been dropped in a merge somewhere...
/-- A block matrix is invertible if the bottom right corner and the corresponding schur complement | ||
is. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Somewhere in this file you can add a cross-reference (and I guess in the other direction too!) to category_theory.preadditive.biproducts
, which proves very similar results. I guess biprod.guassian and biprod.iso_elim are the most directly relevant ones.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(That is in slightly more generality as it is about 2x2 matrices in a category rather than a ring, but whatever. That file also only does one direction of these invertibility results, and doesn't (I think) give the iff statements.)
This PR/issue depends on: |
bors merge |
…matrices (#19156) Co-authored-by: Jeremy Tan Jie Rui <e0191785@u.nus.edu> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Creating this for the purpose of having an easy diff against #18849