-
Notifications
You must be signed in to change notification settings - Fork 298
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/affine_space/affine_subspace): prove that a set whose affine span is top cannot be empty. #9113
Conversation
…hose affine span is top cannot be empty. The lemma `finset.card_sdiff_add_card` is unrelated but I've been meaning to add it and now seemed like a good time since I'm touching `data/finset/basic.lean` anyway.
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.
LGTM!
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
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.
LGTM modulo a few minor remarks. I see that you're not going to merge it in the next few days, so please merge master and wait for CI before adding it to the queue.
bors d+
bors merge |
…hose affine span is top cannot be empty. (#9113) The lemma `finset.card_sdiff_add_card` is unrelated but I've been meaning to add it and now seemed like a good time since I'm touching `data/finset/basic.lean` anyway.
Pull request successfully merged into master. Build succeeded: |
The lemma
finset.card_sdiff_add_card
is unrelated but I've been meaning to add itand now seemed like a good time since I'm touching
data/finset/basic.lean
anyway.