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 RingTheory.HahnSeries #4261

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: port RingTheory.HahnSeries #4261

wants to merge 13 commits into from

Commits on May 23, 2023

  1. feat: port RingTheory.HahnSeries

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    50f4ca5 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    449b6e0 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
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    42edffe View commit details
    Browse the repository at this point in the history

  4. 800 lines

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    be0dcde View commit details
    Browse the repository at this point in the history

  5. hard proof

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    ea9cb9b View commit details
    Browse the repository at this point in the history

  6. red and yellow

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    c7e1186 View commit details
    Browse the repository at this point in the history

  7. finish red

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    a48f64d View commit details
    Browse the repository at this point in the history

  8. lint

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    017772b View commit details
    Browse the repository at this point in the history

  9. auto: naming

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    d0cf415 View commit details
    Browse the repository at this point in the history

  10. fix one comment

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    c814d2b View commit details
    Browse the repository at this point in the history

  11. isolated by

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    5ebcd13 View commit details
    Browse the repository at this point in the history

  12. fix lint

    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    219b01a View commit details
    Browse the repository at this point in the history

  13. Merge remote-tracking branch 'origin/master' into port/RingTheory.Hah… 

    …nSeries
    @ChrisHughes24
    ChrisHughes24 committed May 23, 2023
    Configuration menu
    Copy the full SHA
    629f2d5 View commit details
    Browse the repository at this point in the history