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] - feat: port ModelTheory.Substructures #3913

Closed
wants to merge 47 commits into from

Commits on Mar 30, 2023

  1. Configuration menu
    Copy the full SHA
    a6e1e9d View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    4841b4d View commit details
    Browse the repository at this point in the history
  3. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    d93a4c4 View commit details
    Browse the repository at this point in the history
  4. fix red

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    a3b2ed9 View commit details
    Browse the repository at this point in the history
  5. fix yellow

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    e088b3b View commit details
    Browse the repository at this point in the history
  6. line length

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    81a2cf1 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    27d42ff View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    5ef5f0f View commit details
    Browse the repository at this point in the history
  9. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    dc91b5f View commit details
    Browse the repository at this point in the history
  10. fix red

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    2a0b1fb View commit details
    Browse the repository at this point in the history
  11. fix yellow

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    49add2c View commit details
    Browse the repository at this point in the history
  12. remove warnings

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    b0a3a69 View commit details
    Browse the repository at this point in the history
  13. auto: naming

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    3bf908a View commit details
    Browse the repository at this point in the history
  14. more comment fixing

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    e3a1ebb View commit details
    Browse the repository at this point in the history
  15. line length

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    c16b8c2 View commit details
    Browse the repository at this point in the history
  16. naming and fix aligns

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    151960b View commit details
    Browse the repository at this point in the history
  17. Configuration menu
    Copy the full SHA
    472f2eb View commit details
    Browse the repository at this point in the history
  18. fix build

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    06e1f3b View commit details
    Browse the repository at this point in the history
  19. Configuration menu
    Copy the full SHA
    37b352a View commit details
    Browse the repository at this point in the history
  20. Configuration menu
    Copy the full SHA
    8a68092 View commit details
    Browse the repository at this point in the history
  21. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    1acb8f1 View commit details
    Browse the repository at this point in the history
  22. start fixing

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    b90ee30 View commit details
    Browse the repository at this point in the history
  23. more progress

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    644b138 View commit details
    Browse the repository at this point in the history
  24. fixes

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    b48db48 View commit details
    Browse the repository at this point in the history
  25. fix yellow

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    b7d03aa View commit details
    Browse the repository at this point in the history
  26. fix comments

    ChrisHughes24 committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    744ca07 View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2023

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

Commits on Apr 3, 2023

  1. add simp lemma

    ChrisHughes24 committed Apr 3, 2023
    Configuration menu
    Copy the full SHA
    d371728 View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2023

  1. Configuration menu
    Copy the full SHA
    d7d4317 View commit details
    Browse the repository at this point in the history
  2. fix a little

    ChrisHughes24 committed Apr 17, 2023
    Configuration menu
    Copy the full SHA
    8de6dc3 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2023

  1. Configuration menu
    Copy the full SHA
    7a55451 View commit details
    Browse the repository at this point in the history
  2. fix

    Komyyy committed May 10, 2023
    Configuration menu
    Copy the full SHA
    9c5a8c8 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2023

  1. fix

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    1488c89 View commit details
    Browse the repository at this point in the history
  2. fix

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    83f0ec2 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    6b1da97 View commit details
    Browse the repository at this point in the history
  4. fix

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    63137e0 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    114192a View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    4c17502 View commit details
    Browse the repository at this point in the history
  7. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    5f56f01 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    e4fde9a View commit details
    Browse the repository at this point in the history
  9. fix

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    b594922 View commit details
    Browse the repository at this point in the history
  10. fix

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    bcabcd0 View commit details
    Browse the repository at this point in the history
  11. isolated by

    Komyyy committed May 11, 2023
    Configuration menu
    Copy the full SHA
    92c6221 View commit details
    Browse the repository at this point in the history

Commits on May 12, 2023

  1. Configuration menu
    Copy the full SHA
    26aed0a View commit details
    Browse the repository at this point in the history
  2. LHom.onTheory_model

    Komyyy committed May 12, 2023
    Configuration menu
    Copy the full SHA
    f627828 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    45879f1 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    7fab5f4 View commit details
    Browse the repository at this point in the history