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(analysis/convex): the gauge as a seminorm over is_R_or_C #14879

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(analysis/convex): the gauge as a seminorm over is_R_or_C #14879

wants to merge 12 commits into from

Commits on Jun 21, 2022

  1. added gauge_smul'

    @mcdoll
    mcdoll committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    f63ead5 View commit details
    Browse the repository at this point in the history

  2. added the rest and corrections

    @mcdoll
    mcdoll committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    3d4ddce View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2022

  1. simplified proof

    @mcdoll
    mcdoll committed Jun 23, 2022
    Configuration menu
    Copy the full SHA
    41aa92f View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2022

  1. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … mcdoll/gauge_complex
    @mcdoll
    mcdoll committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    ad96dc5 View commit details
    Browse the repository at this point in the history

  2. fix

    @mcdoll
    mcdoll committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    0d5e694 View commit details
    Browse the repository at this point in the history

  3. made K explicit

    @mcdoll
    mcdoll committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    8fc6b87 View commit details
    Browse the repository at this point in the history

  4. Revert "made K explicit" 

    This reverts commit 8fc6b87.
    @mcdoll
    mcdoll committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    3a9eb19 View commit details
    Browse the repository at this point in the history

  5. golf

    @mcdoll
    mcdoll committed Jul 9, 2022
    Configuration menu
    Copy the full SHA
    8657b6a View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2022

  1. dedup gauge_seminorm

    @YaelDillies
    YaelDillies committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    c442071 View commit details
    Browse the repository at this point in the history

  2. style

    @YaelDillies
    YaelDillies committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    ed0c8a9 View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2022

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

    @YaelDillies
    YaelDillies committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    9056528 View commit details
    Browse the repository at this point in the history

  2. somehow this got lost

    Moritz Doll committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    4f33610 View commit details
    Browse the repository at this point in the history