Commit 2021-09-22 07:37 b77aa3aa
View on Github →feat(linear_algebra/affine_space/affine_subspace): prove that a set whose 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.