Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces #3377

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces #3377

wants to merge 4 commits into from

Commits on Jul 12, 2020

  1. feat(linear_algebra/affine_space): more lemmas on directions of affin… 

    …e subspaces

Add more lemmas on directions of affine subspaces, motivated by uses
for Euclidean geometry.
    @jsm28
    jsm28 committed Jul 12, 2020
    Configuration menu
    Copy the full SHA
    e2fbf00 View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2020

  1. Update src/linear_algebra/affine_space.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @jsm28 @jcommelin
    jsm28 and jcommelin committed Jul 13, 2020
    Configuration menu
    Copy the full SHA
    53dd3e4 View commit details
    Browse the repository at this point in the history

  2. Update src/linear_algebra/affine_space.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @jsm28 @jcommelin
    jsm28 and jcommelin committed Jul 13, 2020
    Configuration menu
    Copy the full SHA
    342d8fc View commit details
    Browse the repository at this point in the history

  3. Update for renaming.

    @jsm28
    jsm28 committed Jul 13, 2020
    Configuration menu
    Copy the full SHA
    a6eeae0 View commit details
    Browse the repository at this point in the history