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: {Mv}Polynomial.algebraMap_apply simps #11193

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat: {Mv}Polynomial.algebraMap_apply simps #11193

wants to merge 26 commits into from

Commits on Mar 5, 2024

  1. introduce lemma

    @BoltonBailey
    BoltonBailey committed Mar 5, 2024
    Configuration menu
    Copy the full SHA
    fb5b434 View commit details
    Browse the repository at this point in the history

  2. mathc with mvpolynomial

    @BoltonBailey
    BoltonBailey committed Mar 5, 2024
    Configuration menu
    Copy the full SHA
    28a8a17 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. mvpolynomials too

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    632cbc6 View commit details
    Browse the repository at this point in the history

  2. more simps

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    010111f View commit details
    Browse the repository at this point in the history

  3. redundant unfold

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    71a6ce9 View commit details
    Browse the repository at this point in the history

  4. why no fire?

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    b9087a5 View commit details
    Browse the repository at this point in the history

  5. add question

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    5deef97 View commit details
    Browse the repository at this point in the history

  6. fix

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    7c1f4ba View commit details
    Browse the repository at this point in the history

  7. fix ambiguous

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    e2bf955 View commit details
    Browse the repository at this point in the history

  8. should be mv

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    0c58ab9 View commit details
    Browse the repository at this point in the history

  9. fix names

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    86b542a View commit details
    Browse the repository at this point in the history

  10. lix lin

    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    e6aabe4 View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' of https://github.com/leanprover-community/math… 

    …lib4 into BoltonBailey/algebraMap_eq_C
    @BoltonBailey
    BoltonBailey committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    3d61854 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2024

  1. Merge branch 'master' of https://github.com/leanprover-community/math… 

    …lib4 into BoltonBailey/algebraMap_eq_C
    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    0e1b898 View commit details
    Browse the repository at this point in the history

  2. recalculate simp set

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    5d5f3e3 View commit details
    Browse the repository at this point in the history

  3. unneeded lemma

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    4463b6f View commit details
    Browse the repository at this point in the history

  4. fix proof

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    8dd6c4c View commit details
    Browse the repository at this point in the history

  5. add only

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    2da28b7 View commit details
    Browse the repository at this point in the history

  6. restore old proof

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    3372e60 View commit details
    Browse the repository at this point in the history

  7. golf

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    7eb7ae7 View commit details
    Browse the repository at this point in the history

  8. remove simps proved

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    15c48e8 View commit details
    Browse the repository at this point in the history

  9. remove more simps

    @BoltonBailey
    BoltonBailey committed Mar 24, 2024
    Configuration menu
    Copy the full SHA
    76a8438 View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2024

  1. Merge branch 'master' of https://github.com/leanprover-community/math… 

    …lib4 into BoltonBailey/algebraMap_eq_C
    @BoltonBailey
    BoltonBailey committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    1921438 View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2024

  1. Update Equiv.lean

    @BoltonBailey
    BoltonBailey committed Apr 9, 2024
    Configuration menu
    Copy the full SHA
    1fe9f0a View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2024

  1. Merge remote-tracking branch 'origin/master' into BoltonBailey/algebr… 

    …aMap_eq_C
    @fpvandoorn
    fpvandoorn committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    d7606ee View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/leanprover-community/math… 

    …lib4 into BoltonBailey/algebraMap_eq_C
    @BoltonBailey
    BoltonBailey committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    b3d658c View commit details
    Browse the repository at this point in the history