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): add WithLp for products #6136

Closed
wants to merge 48 commits into from
Closed

[Merged by Bors] - feat(Analysis): add WithLp for products #6136

wants to merge 48 commits into from

Commits on Jul 25, 2023

  1. ProdLp, first quarter or so

    @mcdoll
    mcdoll committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    793c15c View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. two proofs

    @mcdoll
    mcdoll committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    fb9744c View commit details
    Browse the repository at this point in the history

  2. more fixes

    @mcdoll
    mcdoll committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    3288d03 View commit details
    Browse the repository at this point in the history

  3. half way point

    @mcdoll
    mcdoll committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    b5e8424 View commit details
    Browse the repository at this point in the history

Commits on Aug 2, 2023

  1. more stuff

    @mcdoll
    mcdoll committed Aug 2, 2023
    Configuration menu
    Copy the full SHA
    bc719aa View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2023

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

    @mcdoll
    mcdoll committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    d0dd0d9 View commit details
    Browse the repository at this point in the history

  2. fixes

    @mcdoll
    mcdoll committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    ec7429c View commit details
    Browse the repository at this point in the history

  3. stuff

    @mcdoll
    mcdoll committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    b70be84 View commit details
    Browse the repository at this point in the history

  4. last bit for this file?

    @mcdoll
    mcdoll committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    44021a8 View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2023

  1. L2 inner product instance

    @mcdoll
    mcdoll committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    86fda9c View commit details
    Browse the repository at this point in the history

  2. doc-strings

    @mcdoll
    mcdoll committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    2c9f008 View commit details
    Browse the repository at this point in the history

  3. import all files

    @mcdoll
    mcdoll committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    9160bf3 View commit details
    Browse the repository at this point in the history

  4. linter

    @mcdoll
    mcdoll committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    58c0ff7 View commit details
    Browse the repository at this point in the history

  5. old names

    @mcdoll
    mcdoll committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    ab93a9e View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2023

  1. Eric's suggestion

    @mcdoll
    mcdoll committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    5401fc1 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2023

  1. Revert "linter" 

    This reverts commit 58c0ff7.
    @mcdoll
    mcdoll committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    eca9b3f View commit details
    Browse the repository at this point in the history

  2. fixes

    @mcdoll
    mcdoll committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    6a9789b View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2023

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

    @mcdoll
    mcdoll committed Aug 12, 2023
    Configuration menu
    Copy the full SHA
    03e8dfc View commit details
    Browse the repository at this point in the history

  2. fixes

    @mcdoll
    mcdoll committed Aug 12, 2023
    Configuration menu
    Copy the full SHA
    c1a753b View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2023

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

    @mcdoll
    mcdoll committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    0832105 View commit details
    Browse the repository at this point in the history

  2. search and replace

    @mcdoll
    mcdoll committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    63a1aff View commit details
    Browse the repository at this point in the history

  3. fixed Type*

    @mcdoll
    mcdoll committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    49df75a View commit details
    Browse the repository at this point in the history

  4. linter

    @mcdoll
    mcdoll committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    7703091 View commit details
    Browse the repository at this point in the history

  5. naming

    @mcdoll
    mcdoll committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    28ac6a5 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2023

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

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    ee3708d View commit details
    Browse the repository at this point in the history

  2. moved algebra lemmas up

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    beace9e View commit details
    Browse the repository at this point in the history

  3. simple corrections

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    e15ece9 View commit details
    Browse the repository at this point in the history

  4. more suggestions

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    1a864f6 View commit details
    Browse the repository at this point in the history

  5. removed porting notes

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    e49da98 View commit details
    Browse the repository at this point in the history

  6. more corrections

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    e0048b9 View commit details
    Browse the repository at this point in the history

  7. more corrections

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    daabeab View commit details
    Browse the repository at this point in the history

  8. more instances and rearranging

    @mcdoll
    mcdoll committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    17d9d2b View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2023

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

    @mcdoll
    mcdoll committed Aug 17, 2023
    Configuration menu
    Copy the full SHA
    4b6d4b2 View commit details
    Browse the repository at this point in the history

  2. naming

    @mcdoll
    mcdoll committed Aug 17, 2023
    Configuration menu
    Copy the full SHA
    8d85e4a View commit details
    Browse the repository at this point in the history

  3. doc-string and examples

    @mcdoll
    mcdoll committed Aug 17, 2023
    Configuration menu
    Copy the full SHA
    1c28a30 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2023

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

    @mcdoll
    mcdoll committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    2334034 View commit details
    Browse the repository at this point in the history

  2. corrections

    @mcdoll
    mcdoll committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    1d9a269 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/NormedSpace/ProdLp.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mcdoll @eric-wieser
    mcdoll and eric-wieser committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    a06efda View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2023

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

    @mcdoll
    mcdoll committed Sep 2, 2023
    Configuration menu
    Copy the full SHA
    29643c1 View commit details
    Browse the repository at this point in the history

  2. corrections

    @mcdoll
    mcdoll committed Sep 2, 2023
    Configuration menu
    Copy the full SHA
    874ef83 View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2023

  1. Sebastien's suggestions

    @mcdoll
    mcdoll committed Sep 7, 2023
    Configuration menu
    Copy the full SHA
    1436977 View commit details
    Browse the repository at this point in the history

  2. one easy typeclass golf

    @mcdoll
    mcdoll committed Sep 7, 2023
    Configuration menu
    Copy the full SHA
    8abe9b0 View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2023

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

    @mcdoll
    mcdoll committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    22a6447 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2023

  1. move norm_of L2 section back to ProdLp

    @mcdoll
    mcdoll committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    c966caa View commit details
    Browse the repository at this point in the history

  2. fix lint

    @eric-wieser
    eric-wieser committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    dadffb9 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2023

  1. coherence

    @mcdoll
    mcdoll committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    48c7e02 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'mcdoll/inner_prod_prod' of github.com:leanprover-commun… 

    …ity/mathlib4 into mcdoll/inner_prod_prod
    @mcdoll
    mcdoll committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    7cdce1f View commit details
    Browse the repository at this point in the history

  3. lint

    @mcdoll
    mcdoll committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    78ee3b0 View commit details
    Browse the repository at this point in the history