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: port Algebra.MonoidAlgebra.Division #3068

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: port Algebra.MonoidAlgebra.Division #3068

wants to merge 19 commits into from

Commits on Mar 23, 2023

  1. chore: forward-port leanprover-community#15905

    @eric-wieser
    eric-wieser committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    0966ba5 View commit details
    Browse the repository at this point in the history

  2. sha

    @eric-wieser
    eric-wieser committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    f805c84 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2023

  1. feat: port Algebra.MonoidAlgebra.Division

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    00d2c04 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    f7980ac 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
    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    9511106 View commit details
    Browse the repository at this point in the history

  4. Fix some errors

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    72918a4 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'forward-port-15905' into port/Algebra.MonoidAlgebra.Div… 

    …ision
    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    ae701c7 View commit details
    Browse the repository at this point in the history

  6. Fix long lines

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    0c3f755 View commit details
    Browse the repository at this point in the history

  7. Revert changes to Data/Polynomial/Inductions

    @Parcly-Taxel
    Parcly-Taxel committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    b37f5b4 View commit details
    Browse the repository at this point in the history

Commits on Mar 25, 2023

  1. Merge branch 'master' into port/Algebra.MonoidAlgebra.Division

    @Parcly-Taxel
    Parcly-Taxel committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    fdf7b33 View commit details
    Browse the repository at this point in the history

  2. Manually add new theorem

    @Parcly-Taxel
    Parcly-Taxel committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    680cf0f View commit details
    Browse the repository at this point in the history

  3. feat: port Algebra.MonoidAlgebra.Division

    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    b281170 View commit details
    Browse the repository at this point in the history

  4. Initial file copy from mathport

    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    b99264f View commit details
    Browse the repository at this point in the history

  5. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    d5cc4c8 View commit details
    Browse the repository at this point in the history

  6. Merge commit 'd5cc4c80aec9b1431bc885ee18b9adce798fa42d' into port/Alg… 

    …ebra.MonoidAlgebra.Division
    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    484c424 View commit details
    Browse the repository at this point in the history

  7. fix build

    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    72c6340 View commit details
    Browse the repository at this point in the history

  8. better porting note

    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    294b1a2 View commit details
    Browse the repository at this point in the history

  9. remove debug line, whoops

    @eric-wieser
    eric-wieser committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    5b19057 View commit details
    Browse the repository at this point in the history

  10. simp can prove this

    @Parcly-Taxel
    Parcly-Taxel committed Mar 25, 2023
    Configuration menu
    Copy the full SHA
    28c5f5d View commit details
    Browse the repository at this point in the history