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.

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

[Merged by Bors] - chore(topology/algebra/ordered): move code, add missing lemmas #5481

Closed
wants to merge 15 commits into from

Commits on Dec 21, 2020

  1. Snapshot

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    b94569e View commit details
    Browse the repository at this point in the history
  2. chore(order/filter/basic): make univ_mem_sets a simp lemma

    Also add `@[simp]` to `rel.core_univ`.
    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    ea53f4e View commit details
    Browse the repository at this point in the history
  3. Snapshot

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    d14f067 View commit details
    Browse the repository at this point in the history
  4. Fix

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    0b6a7c4 View commit details
    Browse the repository at this point in the history
  5. Fix, golf

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    d5dafce View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    19ad651 View commit details
    Browse the repository at this point in the history
  7. Snapshot

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    0ca6deb View commit details
    Browse the repository at this point in the history
  8. Split long lines

    urkud committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    f572d0b View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    ce18236 View commit details
    Browse the repository at this point in the history

Commits on Dec 22, 2020

  1. Fix

    urkud committed Dec 22, 2020
    Configuration menu
    Copy the full SHA
    fea8278 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    f3fa7c0 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    91fc79e View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    a7d337c View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    3d2d124 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2020

  1. Configuration menu
    Copy the full SHA
    a462404 View commit details
    Browse the repository at this point in the history