mathlib

b77aa3aa - feat(linear_algebra/affine_space/affine_subspace): prove that a set whose affine span is top cannot be empty. (#9113)

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.