-
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(data/matrix/rank): rank of multiplication #18784
Conversation
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.
Thanks!
bors d+
src/data/matrix/rank.lean
Outdated
lemma rank_mul_le_right [strong_rank_condition R] (A : matrix l m R) (B : matrix m n R) : | ||
(A ⬝ B).rank ≤ B.rank := | ||
begin | ||
classical, |
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.
Why do we need classical
here and not in the proof of rank_mul_le_left
?
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.
Because to_lin'_mul
is asymmetric in which arguments it needs decidable equality in (the truth is that it doesn't need it at all, but that's a refactor for another time).
I've changed this to a letI
to make the reason clearer.
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.
The "another time" is now: #18800
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
This adds a universe-polymorphic version of `rank_comp_le_right`, and then uses it to show `(A ⬝ B).rank ≤ B.rank`; previously we only had `(A ⬝ B).rank ≤ A.rank`. For convenience, this adds the spellings `(A ⬝ B).rank ≤ min A.rank B.rank` and `rank (f.comp g) ≤ min (rank f) (rank g)`, as these map well to the way that rank would be described in words.
Pull request successfully merged into master. Build succeeded: |
This adds a universe-polymorphic version of
rank_comp_le_right
, and then uses it to show(A ⬝ B).rank ≤ B.rank
; previously we only had(A ⬝ B).rank ≤ A.rank
.For convenience, this adds the spellings
(A ⬝ B).rank ≤ min A.rank B.rank
andrank (f.comp g) ≤ min (rank f) (rank g)
, as these map well to the way that rank would be described in words.