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/finite_dimensional): Define rank of set of vectors #11290
Conversation
There are also a few more occurrences of |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Looks like the proof of
|
I reverted the modifications, that decision was also echoed in zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/First.20Time.20Contributing/near/267238587 |
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 merge
@cuppajoeman Would you mind making a follow-up PR with simp-lemmas about |
#11290) Added in the definition of "rank of a set of vectors" and a useful lemma about the rank when one set is a subset of the other. Read the zulip stream here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/First.20Time.20Contributing Co-authored-by: ccn <callum.cassidynolan@mail.utoronto.ca>
Pull request successfully merged into master. Build succeeded: |
Hey, sorry I just checked in on this PR again, did you still need this to happen? |
Added in the definition of "rank of a set of vectors" and a useful lemma about the rank when one set is a subset of the other.
Read the zulip stream here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/First.20Time.20Contributing