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/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems #2819

Closed
wants to merge 189 commits into from
Closed

[Merged by Bors] - feat(measure_theory/group/geometry_of_numbers): Blichfeldt and Minkowski's theorems #2819

wants to merge 189 commits into from

Commits on May 25, 2020

  1. initial go at minkowski

    @alexjbest
    alexjbest committed May 25, 2020
    Configuration menu
    Copy the full SHA
    b7a3d73 View commit details
    Browse the repository at this point in the history

  2. not needed?

    @alexjbest
    alexjbest committed May 25, 2020
    Configuration menu
    Copy the full SHA
    b7cf41a View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2020

  1. Delete probability_theory.lean

    @alexjbest
    alexjbest committed Nov 1, 2020
    Configuration menu
    Copy the full SHA
    018e2f6 View commit details
    Browse the repository at this point in the history

  2. Delete prod_measure.lean

    @alexjbest
    alexjbest committed Nov 1, 2020
    Configuration menu
    Copy the full SHA
    1e73c64 View commit details
    Browse the repository at this point in the history

  3. Update geometry_of_numbers.lean

    @alexjbest
    alexjbest committed Nov 1, 2020
    Configuration menu
    Copy the full SHA
    5ba26c7 View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2021

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

     into minkowski
    @alexjbest
    alexjbest committed Apr 16, 2021
    Configuration menu
    Copy the full SHA
    df6010a View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2021

  1. get compiling?

    @alexjbest
    alexjbest committed Apr 17, 2021
    Configuration menu
    Copy the full SHA
    243934e View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 6, 2021
    Configuration menu
    Copy the full SHA
    8879baf View commit details
    Browse the repository at this point in the history

  2. refresh

    @alexjbest
    alexjbest committed Aug 6, 2021
    Configuration menu
    Copy the full SHA
    10e7d70 View commit details
    Browse the repository at this point in the history

  3. another lil improvement

    @alexjbest
    alexjbest committed Aug 6, 2021
    Configuration menu
    Copy the full SHA
    5881e56 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2021

  1. cleanup

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    840421a View commit details
    Browse the repository at this point in the history

  2. lint

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    ec27266 View commit details
    Browse the repository at this point in the history

  3. more tidying

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    fbda453 View commit details
    Browse the repository at this point in the history

  4. sorry gone

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    032c749 View commit details
    Browse the repository at this point in the history

  5. more explicit sorries

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    a946c4c View commit details
    Browse the repository at this point in the history

  6. add copy

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    9c2f31f View commit details
    Browse the repository at this point in the history

  7. more tidying

    @alexjbest
    alexjbest committed Aug 7, 2021
    Configuration menu
    Copy the full SHA
    6bfb984 View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2021

  1. one less sorry!

    @alexjbest
    alexjbest committed Aug 8, 2021
    Configuration menu
    Copy the full SHA
    72d3652 View commit details
    Browse the repository at this point in the history

  2. no more sorries

    @alexjbest
    alexjbest committed Aug 8, 2021
    Configuration menu
    Copy the full SHA
    e761f16 View commit details
    Browse the repository at this point in the history

  3. no need to import tactic

    @alexjbest
    alexjbest committed Aug 8, 2021
    Configuration menu
    Copy the full SHA
    39d0e3a View commit details
    Browse the repository at this point in the history

  4. cleanup

    @alexjbest
    alexjbest committed Aug 8, 2021
    Configuration menu
    Copy the full SHA
    400c091 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2021

  1. more tidying, and universe issues

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    1746771 View commit details
    Browse the repository at this point in the history

  2. generalize

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    fc7697c View commit details
    Browse the repository at this point in the history

  3. fix proof

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    cb11bb3 View commit details
    Browse the repository at this point in the history

  4. linting and cleaning

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    7db97eb View commit details
    Browse the repository at this point in the history

  5. reducing imports

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    4290ed7 View commit details
    Browse the repository at this point in the history

  6. no specific references were followed

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    e3f5b80 View commit details
    Browse the repository at this point in the history

  7. lemmas on smul of intervals

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    e7bcca9 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'alexjbest/smul_interval' of github.com:leanprover-commu… 

    …nity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    cfd9eac View commit details
    Browse the repository at this point in the history

  9. base off smul_interval

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    51524c2 View commit details
    Browse the repository at this point in the history

  10. module doc

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    d2f6413 View commit details
    Browse the repository at this point in the history

  11. Merge branch 'alexjbest/smul_interval' of github.com:leanprover-commu… 

    …nity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    990f334 View commit details
    Browse the repository at this point in the history

  12. randomly generalise some stuff

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    eabf1d3 View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    3357924 View commit details
    Browse the repository at this point in the history

  14. long lines

    @alexjbest
    alexjbest committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    745f82a View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2021

  1. add preimage_smul and generalize

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    82f058d View commit details
    Browse the repository at this point in the history

  2. reorganize and add doc

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    0590d6d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'alexjbest/preimage_smul' of github.com:leanprover-commu… 

    …nity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    b9fe65a View commit details
    Browse the repository at this point in the history

  4. update

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    45608a5 View commit details
    Browse the repository at this point in the history

  5. Update src/algebra/pointwise.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @alexjbest @eric-wieser
    alexjbest and eric-wieser committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    021e1ad View commit details
    Browse the repository at this point in the history

  6. Update src/algebra/pointwise.lean

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    d29b1eb View commit details
    Browse the repository at this point in the history

  7. more generalization and cleanup

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    ecaeb00 View commit details
    Browse the repository at this point in the history

  8. more cleanup

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    fc36340 View commit details
    Browse the repository at this point in the history

  9. generalize and reorganize

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    841c815 View commit details
    Browse the repository at this point in the history

  10. refactor to generalise

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    c88aa4f View commit details
    Browse the repository at this point in the history

  11. generalise pi type

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    00ad99e View commit details
    Browse the repository at this point in the history

  12. add smul_add_smul

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    26845cc View commit details
    Browse the repository at this point in the history

  13. line

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    58b4e58 View commit details
    Browse the repository at this point in the history

  14. Merge branch 'alexjbest/smul_set_add' of github.com:leanprover-commun… 

    …ity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    a4596e4 View commit details
    Browse the repository at this point in the history

  15. base off smul_set_add

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    bfb818c View commit details
    Browse the repository at this point in the history

  16. remove extra fiel

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    7e7b32b View commit details
    Browse the repository at this point in the history

  17. Update src/algebra/pointwise.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @alexjbest @eric-wieser
    alexjbest and eric-wieser committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    8e1fda5 View commit details
    Browse the repository at this point in the history

  18. Update src/algebra/pointwise.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @alexjbest @eric-wieser
    alexjbest and eric-wieser committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    81d2de8 View commit details
    Browse the repository at this point in the history

  19. eric's suggestions

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    c5929d3 View commit details
    Browse the repository at this point in the history

  20. Merge branch 'alexjbest/preimage_smul' of github.com:leanprover-commu… 

    …nity/mathlib into alexjbest/preimage_smul
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    9ce1f79 View commit details
    Browse the repository at this point in the history

  21. Update src/algebra/pointwise.lean 

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

  22. generalise to le

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    e576cb5 View commit details
    Browse the repository at this point in the history

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

    … alexjbest/smul_set_add
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    e4b81db View commit details
    Browse the repository at this point in the history

  24. reflow

    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    f55699e View commit details
    Browse the repository at this point in the history

  25. Merge branch 'alexjbest/smul_set_add' of github.com:leanprover-commun… 

    …ity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    455155d View commit details
    Browse the repository at this point in the history

  26. Merge branch 'alexjbest/preimage_smul' of github.com:leanprover-commu… 

    …nity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 10, 2021
    Configuration menu
    Copy the full SHA
    10cd674 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2021

  1. Update src/analysis/convex/basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @alexjbest @eric-wieser
    alexjbest and eric-wieser committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    2c2f905 View commit details
    Browse the repository at this point in the history

  2. flip proof

    @alexjbest
    alexjbest committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    eb9f1ea View commit details
    Browse the repository at this point in the history

  3. more generalization

    @alexjbest
    alexjbest committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    6bb1dd4 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'alexjbest/smul_set_add' of github.com:leanprover-commun… 

    …ity/mathlib into minkowski
    @alexjbest
    alexjbest committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    c5c0d79 View commit details
    Browse the repository at this point in the history

  5. adjust upstream

    @alexjbest
    alexjbest committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    d97854a View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    fc19e38 View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2021

  1. interior_pi

    @alexjbest
    alexjbest committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    46c2873 View commit details
    Browse the repository at this point in the history

  2. break out general part

    @alexjbest
    alexjbest committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    aca5e8b View commit details
    Browse the repository at this point in the history

  3. Merge branch 'interior_pi' of github.com:leanprover-community/mathlib… 

    … into minkowski
    @alexjbest
    alexjbest committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    56cba8c View commit details
    Browse the repository at this point in the history

  4. fix

    @alexjbest
    alexjbest committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    ca86ca7 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'interior_pi' of github.com:leanprover-community/mathlib… 

    … into minkowski
    @alexjbest
    alexjbest committed Aug 12, 2021
    Configuration menu
    Copy the full SHA
    d726584 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 13, 2021
    Configuration menu
    Copy the full SHA
    d5e1d2a View commit details
    Browse the repository at this point in the history

  2. update to match interior_pi

    @alexjbest
    alexjbest committed Aug 13, 2021
    Configuration menu
    Copy the full SHA
    b359cdc View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2021

  1. feat(topology): interior of a finite product of sets 

    Also finishes the filter inf work from #8657 proving stronger lemmas for
filter.infi
    @PatrickMassot
    PatrickMassot committed Aug 15, 2021
    Configuration menu
    Copy the full SHA
    81707e3 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 16, 2021
    Configuration menu
    Copy the full SHA
    95b5cbb View commit details
    Browse the repository at this point in the history

  2. remove upstream lemmas

    @alexjbest
    alexjbest committed Aug 16, 2021
    Configuration menu
    Copy the full SHA
    f989ced View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2021

  1. 8 variants of supr_dite

    @jcommelin
    jcommelin committed Aug 21, 2021
    Configuration menu
    Copy the full SHA
    2715570 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2021

  1. Merge branch 'master' into minkowski

    @alexjbest
    alexjbest committed Aug 22, 2021
    Configuration menu
    Copy the full SHA
    57caea4 View commit details
    Browse the repository at this point in the history

  2. Revert "Merge branch 'interior_pi' of github.com:leanprover-community… 

    …/mathlib into minkowski"

This reverts commit d726584, reversing
changes made to 56cba8c.
    @alexjbest
    alexjbest committed Aug 22, 2021
    Configuration menu
    Copy the full SHA
    750560e View commit details
    Browse the repository at this point in the history

  3. Revert "Merge branch 'interior_pi' of github.com:leanprover-community… 

    …/mathlib into minkowski"

This reverts commit 56cba8c, reversing
changes made to fc19e38.
    @alexjbest
    alexjbest committed Aug 22, 2021
    Configuration menu
    Copy the full SHA
    ce65931 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'interior_pi_bis' of github.com:leanprover-community/mat… 

    …hlib into minkowski
    @alexjbest
    alexjbest committed Aug 22, 2021
    Configuration menu
    Copy the full SHA
    ba504dd View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    8bb3e39 View commit details
    Browse the repository at this point in the history

  2. fixup

    @alexjbest
    alexjbest committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    2497219 View commit details
    Browse the repository at this point in the history

  3. attempt to to_additive set smul

    @alexjbest
    alexjbest committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    41475aa View commit details
    Browse the repository at this point in the history

  4. Merge branch 'alexjbest/set_has_vadd' of github.com:leanprover-commun… 

    …ity/mathlib into minkowski-experiments
    @alexjbest
    alexjbest committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    f03a20b View commit details
    Browse the repository at this point in the history

  5. checkpoint

    @alexjbest
    alexjbest committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    d25a68f View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2021

  1. checkpoint again

    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    6039187 View commit details
    Browse the repository at this point in the history

  2. gen

    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    f71d3ca View commit details
    Browse the repository at this point in the history

  3. mul version

    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    008390b View commit details
    Browse the repository at this point in the history

  4. small tidy

    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    e3a71db View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    ff39d42 View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    796f3fc View commit details
    Browse the repository at this point in the history

  7. what is happening

    @alexjbest
    alexjbest committed Aug 30, 2021
    Configuration menu
    Copy the full SHA
    8c52b2c View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2021

  1. working away

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    351ad8c View commit details
    Browse the repository at this point in the history

  2. enable pointwise add_action

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    37b4527 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'alexjbest/pointwise_add_action' into minkowski

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    cf384e3 View commit details
    Browse the repository at this point in the history

  4. tweaks

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    3a0d2ad View commit details
    Browse the repository at this point in the history

  5. checkpoint

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    b54de9c View commit details
    Browse the repository at this point in the history

  6. no need for new line

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    0b57dbe View commit details
    Browse the repository at this point in the history

  7. Merge branch 'alexjbest/pointwise_add_action' into minkowski

    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    d2c2789 View commit details
    Browse the repository at this point in the history

  8. reduce dependence on a subgroup and finish generalizing fundamental d… 

    …omain
    @alexjbest
    alexjbest committed Sep 5, 2021
    Configuration menu
    Copy the full SHA
    aa3023d View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2021

  1. compiling again, refactored in terms of measurable actions better, ra… 

    …ther than explicit subgroups
    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    05036b1 View commit details
    Browse the repository at this point in the history

  2. feat(algebra): add more to_additive attributes for actions

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    1f8d108 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'alexjbest/more-to_additive-for-actions' into minkowski

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    d30d470 View commit details
    Browse the repository at this point in the history

  4. golf

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    ea103ac View commit details
    Browse the repository at this point in the history

  5. get compiling

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    5da3573 View commit details
    Browse the repository at this point in the history

  6. checkpoint

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    7fbcbbb View commit details
    Browse the repository at this point in the history

  7. port other defs too

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    e35c427 View commit details
    Browse the repository at this point in the history

  8. docs

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    6ababd3 View commit details
    Browse the repository at this point in the history

  9. remove lint

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    bd0f704 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'alexjbest/more-to_additive-for-actions' into minkowski

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    208205e View commit details
    Browse the repository at this point in the history

  11. longlines and vrachy

    @alexjbest
    alexjbest committed Sep 6, 2021
    Configuration menu
    Copy the full SHA
    988261b View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2021

  1. fixup haar to_additive was failing as now too additive learned too ma… 

    …ny lemmas
    @alexjbest
    alexjbest committed Sep 7, 2021
    Configuration menu
    Copy the full SHA
    0553a86 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'alexjbest/more-to_additive-for-actions' into minkowski

    @alexjbest
    alexjbest committed Sep 7, 2021
    Configuration menu
    Copy the full SHA
    90a0053 View commit details
    Browse the repository at this point in the history

  3. golfing and cleanup

    @alexjbest
    alexjbest committed Sep 7, 2021
    Configuration menu
    Copy the full SHA
    4e94ea0 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Sep 14, 2021
    Configuration menu
    Copy the full SHA
    9a1e266 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2021

  1. lemma already in mathlib

    @alexjbest
    alexjbest committed Sep 20, 2021
    Configuration menu
    Copy the full SHA
    fec634d View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Sep 24, 2021
    Configuration menu
    Copy the full SHA
    be153fc View commit details
    Browse the repository at this point in the history

  2. update to upstream

    @alexjbest
    alexjbest committed Sep 24, 2021
    Configuration menu
    Copy the full SHA
    5e6968f View commit details
    Browse the repository at this point in the history

  3. another mini generaliztion

    @alexjbest
    alexjbest committed Sep 24, 2021
    Configuration menu
    Copy the full SHA
    74941c1 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2021

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

     into minkowski
    @alexjbest
    alexjbest committed Sep 27, 2021
    Configuration menu
    Copy the full SHA
    dafa159 View commit details
    Browse the repository at this point in the history

  2. some cleanup and update to upstream

    @alexjbest
    alexjbest committed Sep 27, 2021
    Configuration menu
    Copy the full SHA
    21907f1 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2021

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

    … minkowski
    @alexjbest
    alexjbest committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    f21ed6e View commit details
    Browse the repository at this point in the history

  2. refresh branch

    @alexjbest
    alexjbest committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    576cd6e View commit details
    Browse the repository at this point in the history

  3. add an extra random lemma

    @alexjbest
    alexjbest committed Nov 19, 2021
    Configuration menu
    Copy the full SHA
    9cecc2f View commit details
    Browse the repository at this point in the history

Commits on Jan 19, 2022

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

    … minkowski
    @alexjbest
    alexjbest committed Jan 19, 2022
    Configuration menu
    Copy the full SHA
    1e50882 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2022

  1. allmost sorry free again

    @alexjbest
    alexjbest committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    cef2af7 View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    6d272f1 View commit details
    Browse the repository at this point in the history

  3. actually sorry free

    @alexjbest
    alexjbest committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    66e54d4 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2022

  1. lemmaify

    @alexjbest
    alexjbest committed Feb 12, 2022
    Configuration menu
    Copy the full SHA
    d323051 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2022

  1. style

    @alexjbest
    alexjbest committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    b49622d View commit details
    Browse the repository at this point in the history

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

    … minkowski
    @alexjbest
    alexjbest committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    739f546 View commit details
    Browse the repository at this point in the history

  3. fix

    @alexjbest
    alexjbest committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    b222f53 View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2022

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

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

  2. bump, golf

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

Commits on Jul 14, 2022

  1. change comap def

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

  2. lint

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

Commits on Jul 28, 2022

  1. null_measurable_set transported to null_measurable_set

    @RemyDegenne
    RemyDegenne committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    fab4225 View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2022

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

    … minkowski
    @alexjbest
    alexjbest committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    6cd714e View commit details
    Browse the repository at this point in the history

  2. extract sorries

    @alexjbest
    alexjbest committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    8327074 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'minkowski' of github.com:leanprover-community/mathlib i… 

    …nto minkowski
    @alexjbest
    alexjbest committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    97e1bba View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2022

  1. golf a bit

    @alexjbest
    alexjbest committed Sep 8, 2022
    Configuration menu
    Copy the full SHA
    4ad09b8 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2022

  1. simplify and generalize

    @RemyDegenne
    RemyDegenne committed Sep 11, 2022
    Configuration menu
    Copy the full SHA
    bb9d343 View commit details
    Browse the repository at this point in the history

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

    @RemyDegenne
    RemyDegenne committed Sep 11, 2022
    Configuration menu
    Copy the full SHA
    e7f70ec View commit details
    Browse the repository at this point in the history

  3. remove duplicate

    @RemyDegenne
    RemyDegenne committed Sep 11, 2022
    Configuration menu
    Copy the full SHA
    828a61a View commit details
    Browse the repository at this point in the history

  4. fix

    @RemyDegenne
    RemyDegenne committed Sep 11, 2022
    Configuration menu
    Copy the full SHA
    afd99c4 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2022

  1. generalize to non-measurable sets

    @alexjbest
    alexjbest committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    c920529 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into minkowski
    @alexjbest
    alexjbest committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    6ff2268 View commit details
    Browse the repository at this point in the history

  3. little cleanup

    @alexjbest
    alexjbest committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    b48b672 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2022

  1. ready for review

    @RemyDegenne
    RemyDegenne committed Oct 2, 2022
    Configuration menu
    Copy the full SHA
    113dd69 View commit details
    Browse the repository at this point in the history

  2. minor

    @RemyDegenne
    RemyDegenne committed Oct 2, 2022
    Configuration menu
    Copy the full SHA
    d39f765 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2022

  1. sorry free but ugly

    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    56389cd View commit details
    Browse the repository at this point in the history

  2. fix doc

    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    a93c705 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/RD_comap' into minkowski

    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    b2bbadf View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into minkowski
    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    03cc794 View commit details
    Browse the repository at this point in the history

  5. Merge branches 'RD_comap' and 'master' of https://github.com/leanprov… 

    …er-community/mathlib into RD_comap
    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    397a955 View commit details
    Browse the repository at this point in the history

  6. fix after master update

    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    3b307b6 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/RD_comap' into minkowski

    @alexjbest
    alexjbest committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    5078e71 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2022

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

    … minkowski
    @alexjbest
    alexjbest committed Oct 16, 2022
    Configuration menu
    Copy the full SHA
    c4d7315 View commit details
    Browse the repository at this point in the history

  2. cleanup

    @alexjbest
    alexjbest committed Oct 16, 2022
    Configuration menu
    Copy the full SHA
    9a318f2 View commit details
    Browse the repository at this point in the history

  3. more cleanup

    @alexjbest
    alexjbest committed Oct 16, 2022
    Configuration menu
    Copy the full SHA
    4a6d4a6 View commit details
    Browse the repository at this point in the history

  4. encodable-> countable

    @alexjbest
    alexjbest committed Oct 16, 2022
    Configuration menu
    Copy the full SHA
    02c43a3 View commit details
    Browse the repository at this point in the history

Commits on Nov 12, 2022

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

    @YaelDillies
    YaelDillies committed Nov 12, 2022
    Configuration menu
    Copy the full SHA
    8a4f167 View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Nov 12, 2022
    Configuration menu
    Copy the full SHA
    a70fb89 View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2022

  1. bump, golf

    @YaelDillies
    YaelDillies committed Nov 13, 2022
    Configuration menu
    Copy the full SHA
    ae9b46b View commit details
    Browse the repository at this point in the history

  2. dubious to_additive

    @YaelDillies
    YaelDillies committed Nov 13, 2022
    Configuration menu
    Copy the full SHA
    46024a4 View commit details
    Browse the repository at this point in the history

  3. golf further

    @YaelDillies
    YaelDillies committed Nov 13, 2022
    Configuration menu
    Copy the full SHA
    9b29424 View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2022

  1. golf more

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

Commits on Nov 17, 2022

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

    @YaelDillies
    YaelDillies committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    48f9796 View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    13afbe1 View commit details
    Browse the repository at this point in the history

  3. move under measure_theory

    @YaelDillies
    YaelDillies committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    0392647 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2022

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

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    f9fd8cb View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    5c46d5e View commit details
    Browse the repository at this point in the history

  3. subgroup.equiv_map

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    394c593 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into minkowski

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    f080138 View commit details
    Browse the repository at this point in the history

  5. bump

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    c9df723 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/master' into minkowski

    @YaelDillies
    YaelDillies committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    8718e0e View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2022

  1. break long line

    @YaelDillies
    YaelDillies committed Dec 1, 2022
    Configuration menu
    Copy the full SHA
    3b157f0 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2022

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

    @YaelDillies
    YaelDillies committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    87d36f3 View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2023

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

    @YaelDillies
    YaelDillies committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    364aa56 View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    289258c View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2023

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

     into minkowski
    @xroblot
    xroblot committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    0d5281d View commit details
    Browse the repository at this point in the history

  2. new proofs

    @xroblot
    xroblot committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    09ca80e View commit details
    Browse the repository at this point in the history

  3. Small changes

    @xroblot
    xroblot committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    d272f38 View commit details
    Browse the repository at this point in the history

  4. Removed hypothesis

    @xroblot
    xroblot committed Mar 30, 2023
    Configuration menu
    Copy the full SHA
    27e376a View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2023

  1. golf

    @YaelDillies
    YaelDillies committed Mar 31, 2023
    Configuration menu
    Copy the full SHA
    d2d19d2 View commit details
    Browse the repository at this point in the history

  2. generalise null_measurable_set.const_smul

    @YaelDillies
    YaelDillies committed Mar 31, 2023
    Configuration menu
    Copy the full SHA
    4142301 View commit details
    Browse the repository at this point in the history

  3. bibliography

    @YaelDillies
    YaelDillies committed Mar 31, 2023
    Configuration menu
    Copy the full SHA
    49564b8 View commit details
    Browse the repository at this point in the history