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] - refactor(linear_algebra/ray): redefine same_ray to allow zero vectors #12618

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - refactor(linear_algebra/ray): redefine same_ray to allow zero vectors #12618

wants to merge 10 commits into from

Commits on Mar 11, 2022

  1. Snapshot

    @urkud
    urkud committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    f99b380 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into YK-same-ray0

    @urkud
    urkud committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    4b0d202 View commit details
    Browse the repository at this point in the history

  3. Snapshot

    @urkud
    urkud committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    1c7639c View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into YK-same-ray0

    @urkud
    urkud committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    95bc788 View commit details
    Browse the repository at this point in the history

Commits on Mar 12, 2022

  1. Fix lint

    @urkud
    urkud committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    f057c8d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into YK-same-ray0

    @urkud
    urkud committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    c1dc8d7 View commit details
    Browse the repository at this point in the history

  3. Add analysis/normed_space/ray

    @urkud
    urkud committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    281af89 View commit details
    Browse the repository at this point in the history

  4. Update

    @urkud
    urkud committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    11ce39d View commit details
    Browse the repository at this point in the history

  5. Update src/analysis/convex/basic.lean

    @urkud
    urkud committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    93d83be View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2022

  1. Update src/linear_algebra/ray.lean 

    Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
    @urkud @hrmacbeth
    urkud and hrmacbeth committed Mar 13, 2022
    Configuration menu
    Copy the full SHA
    97c04ee View commit details
    Browse the repository at this point in the history