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] - split power series in several files #10866

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - split power series in several files #10866

wants to merge 25 commits into from

Commits on Feb 22, 2024

  1. split power series (some cleanup still needed)

    Antoine Chambert-Loir committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    b8c09e9 View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2024

  1. adjust headers

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    d632cb4 View commit details
    Browse the repository at this point in the history

  2. adjust Mathlib.lean

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    01eb9ad View commit details
    Browse the repository at this point in the history

  3. try to adjust imports of PowerSeries/Derivative

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    a99bcf8 View commit details
    Browse the repository at this point in the history

  4. add import to Bernoulli

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    4b86801 View commit details
    Browse the repository at this point in the history

  5. adjust Archive/Wiedijk100Theorems/Partition

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    3ea748a View commit details
    Browse the repository at this point in the history

  6. adjust import

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    10ffbd6 View commit details
    Browse the repository at this point in the history

  7. adjust import

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    f5d62dc View commit details
    Browse the repository at this point in the history

  8. adjust import (should work this time)

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    b8e8f7c View commit details
    Browse the repository at this point in the history

  9. adjust import

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    f686341 View commit details
    Browse the repository at this point in the history

  10. delete passages that were commented out and copied in other files

    Antoine Chambert-Loir committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    a3f8e1f View commit details
    Browse the repository at this point in the history

Commits on Feb 28, 2024

  1. Merge branch 'master' into ACL/splitPowerSeries

    @jcommelin
    jcommelin committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    4558b56 View commit details
    Browse the repository at this point in the history

  2. remove "-- import …"

    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    375476c View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ACL/splitPowerSeries' of https://github.com/leanprover-… 

    …community/mathlib4 into ACL/splitPowerSeries
    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    833830b View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    1acca95 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    46bb554 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/RingTheory/MvPowerSeries/Inverse.lean 

    Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    20653ef View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/RingTheory/MvPowerSeries/Inverse.lean 

    Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    b08f302 View commit details
    Browse the repository at this point in the history

  8. adjust to Filippo's comments ; add some comments and namespaces in do… 

    …cstring.
    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    3e3acdf View commit details
    Browse the repository at this point in the history

  9. Merge branch 'ACL/splitPowerSeries' of https://github.com/leanprover-… 

    …community/mathlib4 into ACL/splitPowerSeries
    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    4397107 View commit details
    Browse the repository at this point in the history

  10. more comments by Filippo

    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    5797eb1 View commit details
    Browse the repository at this point in the history

  11. adjust for lint 100

    Antoine Chambert-Loir committed Feb 28, 2024
    Configuration menu
    Copy the full SHA
    ad4366f View commit details
    Browse the repository at this point in the history

Commits on Feb 29, 2024

  1. move "Algebra" section after the "CommSemiring" section

    Antoine Chambert-Loir committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    9eaf03a View commit details
    Browse the repository at this point in the history

  2. removed two empty lines

    @faenuccio
    faenuccio committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    703e4b2 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ACL/splitPowerSeries' of https://github.com/leanprover-… 

    …community/mathlib4 into ACL/splitPowerSeries
    @faenuccio
    faenuccio committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    28176f4 View commit details
    Browse the repository at this point in the history