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

feat: liminf and limsup add/mul lemmas in Real #18365

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

feat: liminf and limsup add/mul lemmas in Real #18365

wants to merge 12 commits into from
+338 −55

Commits on Oct 24, 2024

  1. Order lemmas in Group/Fields

    @D-Thomine
    D-Thomine committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    afd42f2 View commit details
    Browse the repository at this point in the history

  2. Swap lemmas

    @D-Thomine
    D-Thomine committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    1325bd8 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. Limsup_add lemmas on reals

    @D-Thomine
    D-Thomine committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    19ce1a8 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. Finish mul lemmas

    @D-Thomine
    D-Thomine committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    8afcf14 View commit details
    Browse the repository at this point in the history

  2. Delete markers

    @D-Thomine
    D-Thomine committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    9584a7b View commit details
    Browse the repository at this point in the history

  3. Lengthen file

    @D-Thomine
    D-Thomine committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    ae9a0c1 View commit details
    Browse the repository at this point in the history

  4. Minimize imports

    @D-Thomine
    D-Thomine committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    00af82f View commit details
    Browse the repository at this point in the history

  5. Remove unnecessary assumptions

    @D-Thomine
    D-Thomine committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    6a8142d View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. Change names and remove docstrings

    @D-Thomine
    D-Thomine committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    946b526 View commit details
    Browse the repository at this point in the history

  2. Golfing Mathlib.Order.LiminfLimsup

    @D-Thomine
    D-Thomine committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    e3d178a View commit details
    Browse the repository at this point in the history

  3. Break up long proof terms

    @D-Thomine
    D-Thomine committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    64ad38a View commit details
    Browse the repository at this point in the history

  4. Eliminate Icos

    @D-Thomine
    D-Thomine committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    1c89dac View commit details
    Browse the repository at this point in the history