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: Extending convex functions #6339

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat: Extending convex functions #6339

wants to merge 18 commits into from

Commits on Aug 3, 2023

  1. feat: Extending convex functions 

    Match leanprover-community/mathlib3#18797
    @YaelDillies
    YaelDillies committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    68d8c1c View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2023

  1. Merge remote-tracking branch 'origin/master' into proj_Ici_convex

    @YaelDillies
    YaelDillies committed Aug 27, 2023
    Configuration menu
    Copy the full SHA
    8063ff2 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2023

  1. fix

    @YaelDillies
    YaelDillies committed Aug 29, 2023
    Configuration menu
    Copy the full SHA
    89c3766 View commit details
    Browse the repository at this point in the history

  2. fix

    @YaelDillies
    YaelDillies committed Aug 29, 2023
    Configuration menu
    Copy the full SHA
    d709c9a View commit details
    Browse the repository at this point in the history

  3. fix analysis.convex.projicc

    @YaelDillies
    YaelDillies committed Aug 29, 2023
    Configuration menu
    Copy the full SHA
    3d82c87 View commit details
    Browse the repository at this point in the history

  4. fix a bit more

    @YaelDillies
    YaelDillies committed Aug 29, 2023
    Configuration menu
    Copy the full SHA
    cef3191 View commit details
    Browse the repository at this point in the history

  5. fix a bit more

    @YaelDillies
    YaelDillies committed Aug 29, 2023
    Configuration menu
    Copy the full SHA
    26118c2 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2023

  1. Eric's comments

    @YaelDillies
    YaelDillies committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    698e75b View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into proj_Ici_convex

    @YaelDillies
    YaelDillies committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    40a024b View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2023

  1. undo ProjIcc

    @YaelDillies
    YaelDillies committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    f5332a0 View commit details
    Browse the repository at this point in the history

  2. fix align

    @YaelDillies
    YaelDillies committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    e4d1aa7 View commit details
    Browse the repository at this point in the history

  3. revert Data.Set.Intervals.Image

    @YaelDillies
    YaelDillies committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    ede0969 View commit details
    Browse the repository at this point in the history

  4. fix all

    @YaelDillies
    YaelDillies committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    fc49843 View commit details
    Browse the repository at this point in the history

  5. revert Data.Set.Intervals.UnorderedInterval

    @YaelDillies
    YaelDillies committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    82f4495 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2023

  1. Add missing align

    @eric-wieser
    eric-wieser authored Sep 13, 2023
    Configuration menu
    Copy the full SHA
    b476ebb View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2023

  1. Merge branch 'master' into proj_Ici_convex

    @eric-wieser
    eric-wieser authored Oct 5, 2023
    Configuration menu
    Copy the full SHA
    d45cd35 View commit details
    Browse the repository at this point in the history

  2. Add aligns

    @eric-wieser
    eric-wieser authored Oct 5, 2023
    Configuration menu
    Copy the full SHA
    14a7c4c View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2023

  1. revert uglification

    @YaelDillies
    YaelDillies committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    db766ae View commit details
    Browse the repository at this point in the history