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 Analysis.Calculus.LHopital #4556

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat: port Analysis.Calculus.LHopital #4556

wants to merge 21 commits into from

Commits on May 30, 2023

  1. Snapshot

    @urkud
    urkud committed May 30, 2023
    Configuration menu
    Copy the full SHA
    bb731ee View commit details
    Browse the repository at this point in the history

  2. Fixes

    @urkud
    urkud committed May 30, 2023
    Configuration menu
    Copy the full SHA
    19e0d6d View commit details
    Browse the repository at this point in the history

Commits on May 31, 2023

  1. feat: port Analysis.Calculus.MeanValue

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    857366f View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    91aea0d 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
    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    09ca957 View commit details
    Browse the repository at this point in the history

  4. Fix, add lemmas about lineMap

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    7e624fa View commit details
    Browse the repository at this point in the history

  5. semiauto: naming

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    c8947cd View commit details
    Browse the repository at this point in the history

  6. Merge branch 'YK-deriv-affine' into port/Analysis.Calculus.MeanValue

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    bd901d4 View commit details
    Browse the repository at this point in the history

  7. Fix

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    8bcdde7 View commit details
    Browse the repository at this point in the history

  8. Add lemmas about lineMap

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    9bd288a View commit details
    Browse the repository at this point in the history

  9. Merge branch 'YK-deriv-affine' into port/Analysis.Calculus.MeanValue

    @urkud
    urkud committed May 31, 2023
    Configuration menu
    Copy the full SHA
    7429013 View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2023

  1. Long line

    @urkud
    urkud committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    3a8ce91 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into port/Analysis.Calcu… 

    …lus.MeanValue
    @fpvandoorn
    fpvandoorn committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    902bd47 View commit details
    Browse the repository at this point in the history

  3. Fix up all the names

    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    c32554d View commit details
    Browse the repository at this point in the history

  4. feat: port Analysis.Calculus.Lhopital

    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    5993c06 View commit details
    Browse the repository at this point in the history

  5. Initial file copy from mathport

    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    1e04bd7 View commit details
    Browse the repository at this point in the history

  6. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    3fdb793 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'port/Analysis.Calculus.MeanValue' into port/Analysis.Ca… 

    …lculus.Lhopital
    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    0f43105 View commit details
    Browse the repository at this point in the history

  8. Fix errors

    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    3f4779d View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into port/Analysis.Calculus.Lhopital

    @Parcly-Taxel
    Parcly-Taxel committed Jun 1, 2023
    Configuration menu
    Copy the full SHA
    5062af1 View commit details
    Browse the repository at this point in the history

Commits on Jun 2, 2023

  1. Update LHopital.lean

    @Parcly-Taxel
    Parcly-Taxel committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    3e603c1 View commit details
    Browse the repository at this point in the history