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(Mathlib/Analysis/SpecificLimits/Basic.lean): add iff versions of lemmas about x^n going to 0 iff x < 1 #11008

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(Mathlib/Analysis/SpecificLimits/Basic.lean): add iff versions of lemmas about x^n going to 0 iff x < 1 #11008

wants to merge 9 commits into from

Commits on Feb 26, 2024

  1. first commit

    @faenuccio
    faenuccio committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    023fc88 View commit details
    Browse the repository at this point in the history

  2. closed main results

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

  3. fixed indentation

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

  4. fixed indentation

    @faenuccio
    faenuccio committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    5cc7086 View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2024

  1. Update Basic.lean

    @Parcly-Taxel
    Parcly-Taxel committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    647cd6d View commit details
    Browse the repository at this point in the history

  2. removed example

    @faenuccio
    faenuccio committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    95bfbfb View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/SpecificLimits/Basic.lean 

    Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
    @faenuccio @MichaelStollBayreuth
    faenuccio and MichaelStollBayreuth committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    4a1e74d View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Analysis/SpecificLimits/Basic.lean 

    Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
    @faenuccio @fpvandoorn
    faenuccio and fpvandoorn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    4cf20c0 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Analysis/SpecificLimits/Basic.lean 

    Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
    @faenuccio @fpvandoorn
    faenuccio and fpvandoorn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    3fd236e View commit details
    Browse the repository at this point in the history