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

feat: Valuative criterion for properness. #14782

Open
wants to merge 38 commits into
base: master
Choose a base branch
from
Open

feat: Valuative criterion for properness. #14782

wants to merge 38 commits into from
+1,735 −0

Commits on Jul 15, 2024

  1. Blueprint of the project

    @erdOne
    erdOne committed Jul 15, 2024
    Configuration menu
    Copy the full SHA
    e1fb7d0 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @erdOne @github-actions
    erdOne and github-actions[bot] authored Jul 15, 2024
    Configuration menu
    Copy the full SHA
    35f560b View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2024

  1. prove isProper_eq

    @jcommelin
    jcommelin committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    62e93ff View commit details
    Browse the repository at this point in the history

  2. close or refine some sorries

    @jcommelin
    jcommelin committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    5bed7eb View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2024

  1. Prove specializingMap

    @GeQi
    GeQi committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    dc1d88b View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. Prove of_specializingMap

    @GeQi
    GeQi committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    eb0c9b8 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2024

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

    @GeQi
    GeQi committed Jul 28, 2024
    Configuration menu
    Copy the full SHA
    52b418c View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. Prove eq

    @GeQi
    GeQi committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    51b0659 View commit details
    Browse the repository at this point in the history

  2. Prove universallyClosed_of_valuativeCriterion and `universallyClose… 

    …d_eq_valuativeCriterion`
    @GeQi
    GeQi committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    fd2f4fe View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2024

  1. Prove stalkClosedPointIso_fromSpecStalk

    @GeQi
    GeQi committed Aug 1, 2024
    Configuration menu
    Copy the full SHA
    aad8639 View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2024

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

    Bump mathlib
    @GeQi
    GeQi committed Aug 10, 2024
    Configuration menu
    Copy the full SHA
    b78fa18 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2024

  1. Fix

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    7aa1d84 View commit details
    Browse the repository at this point in the history

  2. Tidy

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    0348ac6 View commit details
    Browse the repository at this point in the history

  3. Tidy

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    4421b56 View commit details
    Browse the repository at this point in the history

  4. Prove Spec_ofPointTensor_SpecTensorTo

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    803125c View commit details
    Browse the repository at this point in the history

  5. Prove ofPoint_SpectensorTo

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    6fb7277 View commit details
    Browse the repository at this point in the history

  6. Tidy

    @GeQi
    GeQi committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    d29744b View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2024

  1. Finish SpecTensorTo

    @GeQi
    GeQi committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    519c61a View commit details
    Browse the repository at this point in the history

  2. Finish ofPointTensor

    @GeQi
    GeQi committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    c9d74e5 View commit details
    Browse the repository at this point in the history

  3. Finish ofPointtensor_SpectensorTo

    @GeQi
    GeQi committed Aug 12, 2024
    Configuration menu
    Copy the full SHA
    3a26f28 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2024

  1. Prove carrierEquiv

    @GeQi
    GeQi committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    5ebd36d View commit details
    Browse the repository at this point in the history

  2. Tidy

    @GeQi
    GeQi committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    0385af4 View commit details
    Browse the repository at this point in the history

  3. Fix

    @GeQi
    GeQi committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    d93983d View commit details
    Browse the repository at this point in the history

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

    @GeQi
    GeQi committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    cd0da94 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. fill some sorries

    @chrisflav
    chrisflav committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    3bb0fd8 View commit details
    Browse the repository at this point in the history

  2. fix one more sorry

    @chrisflav
    chrisflav committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    2745be4 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. prove ispreimmersion

    @chrisflav
    chrisflav committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    cfd76f4 View commit details
    Browse the repository at this point in the history

  2. fill more sorries

    @chrisflav
    chrisflav committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    9282779 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. finish universally closed

    @chrisflav
    chrisflav committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    9207420 View commit details
    Browse the repository at this point in the history

  2. rename valuation ring

    @chrisflav
    chrisflav committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    bcb683a View commit details
    Browse the repository at this point in the history

  3. complete valuative criterion file

    @chrisflav
    chrisflav committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    d1ea7a8 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2024

  1. last sorry in pullback carrier

    @chrisflav
    chrisflav committed Oct 11, 2024
    Configuration menu
    Copy the full SHA
    13ed04b View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. add pr notices

    @chrisflav
    chrisflav committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    742d3b4 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

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

    …lib4 into valuativeCriterion
    @erdOne
    erdOne committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    e61c33c View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2024

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

    …lib4 into valuativeCriterion
    @erdOne
    erdOne committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    fda4bff View commit details
    Browse the repository at this point in the history

  2. bump mathlib

    @erdOne
    erdOne committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    219079e View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2024

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

    …lib4 into valuativeCriterion
    @erdOne
    erdOne committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    53f86a0 View commit details
    Browse the repository at this point in the history

  2. bump

    @erdOne
    erdOne committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    e7c9083 View commit details
    Browse the repository at this point in the history