Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

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

Closed
wants to merge 3 commits into from
Closed

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

wants to merge 3 commits into from

Commits on Sep 9, 2021

  1. feat(linear_algebra/affine_space/affine_subspace): prove that a set w… 

    …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.
    @ocfnash
    ocfnash committed Sep 9, 2021
    Configuration menu
    Copy the full SHA
    0127550 View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2021

  1. Merge branch 'master' into affine_subspace_lemmas

    @ocfnash
    ocfnash committed Sep 21, 2021
    Configuration menu
    Copy the full SHA
    7ff66d3 View commit details
    Browse the repository at this point in the history

  2. Suggestions from CR

    @ocfnash
    ocfnash committed Sep 21, 2021
    Configuration menu
    Copy the full SHA
    d32df80 View commit details
    Browse the repository at this point in the history