-
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/determinant): generalize det_fin_zero to det_eq_one_of_is_empty #8387
Conversation
…et_eq_one_of_is_empty Also golfs a nearby proof
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.
Have you tried showing det_eq_one_of_is_empty
directly? Ideally it would be at least as easy as det_eq_one_of_card_eq_zero
, so if it is more difficult that would suggest that there are some missing lemmas.
The generalization looks good to me otherwise.
We were missing the |
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.
Looks good to me, thanks for fixing all the dependencies!
bors r+
…et_eq_one_of_is_empty (#8387) Also golfs a nearby proof
Pull request successfully merged into master. Build succeeded: |
Also golfs a nearby proof