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(measure_theory/lp_space): add snorm_norm_rpow #6619

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(measure_theory/lp_space): add snorm_norm_rpow #6619

wants to merge 8 commits into from

Commits on Mar 10, 2021

  1. snorm_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    9804605 View commit details
    Browse the repository at this point in the history

  2. change the name of a variable

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    b3374d3 View commit details
    Browse the repository at this point in the history

  3. remove a lemma

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    96c9883 View commit details
    Browse the repository at this point in the history

  4. replace pos hypothesis with nonneg

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    e95a0cb View commit details
    Browse the repository at this point in the history

  5. reorder proof

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    a2eb745 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2021

  1. G -> F

    @RemyDegenne
    RemyDegenne committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    aa46ac8 View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2021

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

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    2229f9f View commit details
    Browse the repository at this point in the history

  2. remove duplicate lemma

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    fc5e2d5 View commit details
    Browse the repository at this point in the history