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(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity #9618

Closed
wants to merge 29 commits into from
Closed

[Merged by Bors] - feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): fromSpec and toSpec compose to identity #9618

wants to merge 29 commits into from

Commits on Jan 8, 2024

  1. initial

    @jjaassoonn
    jjaassoonn committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    5fbc6dc View commit details
    Browse the repository at this point in the history

Commits on Jan 9, 2024

  1. initial

    @jjaassoonn
    jjaassoonn committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    041916e View commit details
    Browse the repository at this point in the history

  2. rename

    @jjaassoonn
    jjaassoonn committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    37298fe View commit details
    Browse the repository at this point in the history

  3. Merge branch 'zjj/DirectSum/Decomposition/degree_eq_of_mem_mem' into … 

    …zjj/projConstruction
    @jjaassoonn
    jjaassoonn committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    a8bcd6a View commit details
    Browse the repository at this point in the history

  4. remove sorry

    @jjaassoonn
    jjaassoonn committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    8c7e244 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @jjaassoonn @github-actions
    jjaassoonn and github-actions[bot] committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    cb48d4e View commit details
    Browse the repository at this point in the history

  6. slight golf

    @jjaassoonn
    jjaassoonn committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    b82da44 View commit details
    Browse the repository at this point in the history

Commits on Jan 10, 2024

  1. Merge branch 'master' into zjj/projConstruction

    @Parcly-Taxel
    Parcly-Taxel committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    e37121c View commit details
    Browse the repository at this point in the history

  2. one sorry

    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    75b59ac View commit details
    Browse the repository at this point in the history

  3. sorry free

    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    514cac6 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into projConstruction/fr… 

    …omSpecToSpec
    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    74b9a01 View commit details
    Browse the repository at this point in the history

  5. 更新 Scheme.lean

    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    b717751 View commit details
    Browse the repository at this point in the history

  6. 更新 Scheme.lean

    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    a2fc57b View commit details
    Browse the repository at this point in the history

  7. 更新 Scheme.lean

    @jjaassoonn
    jjaassoonn committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    826ceca View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2024

  1. golf

    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    1c1bffb View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/zjj/projConstruction' into projC… 

    …onstruction/fromSpecToSpec
    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    122d7b0 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'projConstruction/fromSpecToSpec' of https://github.com/… 

    …leanprover-community/mathlib4 into projConstruction/fromSpecToSpec
    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    74cec6b View commit details
    Browse the repository at this point in the history

  4. Update Scheme.lean

    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    161428e View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into projConstruction/fr… 

    …omSpecToSpec
    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    fec1a5a View commit details
    Browse the repository at this point in the history

  6. golf

    @jjaassoonn
    jjaassoonn committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    18d1c8f View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2024

  1. Merge remote-tracking branch 'origin/master' into projConstruction/fr… 

    …omSpecToSpec
    @jjaassoonn
    jjaassoonn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    d6b9414 View commit details
    Browse the repository at this point in the history

  2. Update Scheme.lean

    @jjaassoonn
    jjaassoonn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    a5d462f View commit details
    Browse the repository at this point in the history

  3. fix

    @jjaassoonn
    jjaassoonn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    0dbaef7 View commit details
    Browse the repository at this point in the history

  4. minimize diff

    @jjaassoonn
    jjaassoonn committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    eb45b78 View commit details
    Browse the repository at this point in the history

Commits on Feb 29, 2024

  1. 更新 Scheme.lean 

    Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
    @jjaassoonn @erdOne
    jjaassoonn and erdOne committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    8ca8ba8 View commit details
    Browse the repository at this point in the history

  2. fix

    @jjaassoonn
    jjaassoonn committed Feb 29, 2024
    Configuration menu
    Copy the full SHA
    6a1d884 View commit details
    Browse the repository at this point in the history

Commits on Mar 1, 2024

  1. Apply suggestions from code review 

    Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
    @jjaassoonn @riccardobrasca
    jjaassoonn and riccardobrasca committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    085ebb5 View commit details
    Browse the repository at this point in the history

  2. fix

    @jjaassoonn
    jjaassoonn committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    8d640c5 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into projConstruction/fr… 

    …omSpecToSpec
    @jjaassoonn
    jjaassoonn committed Mar 1, 2024
    Configuration menu
    Copy the full SHA
    bec2b79 View commit details
    Browse the repository at this point in the history