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(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

Closed
wants to merge 65 commits into from
Closed

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

wants to merge 65 commits into from

Commits on Apr 19, 2024

  1. 1st commit

    @xroblot
    xroblot committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    1dd37b7 View commit details
    Browse the repository at this point in the history

  2. Typos

    @xroblot
    xroblot committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    6f34395 View commit details
    Browse the repository at this point in the history

  3. Lint

    @xroblot
    xroblot committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    01b097f View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2024

  1. Backport changes

    @xroblot
    xroblot committed Apr 21, 2024
    Configuration menu
    Copy the full SHA
    6b5c3d0 View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2024

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

    …e_def
    @xroblot
    xroblot committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    8053571 View commit details
    Browse the repository at this point in the history

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

    …e_def
    @xroblot
    xroblot committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    2ab05a8 View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2024

  1. Remove instance

    @xroblot
    xroblot committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    dee6067 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2024

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

    …e_def
    @xroblot
    xroblot committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    a054ea1 View commit details
    Browse the repository at this point in the history

  2. Docs

    @xroblot
    xroblot committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    97eb8e9 View commit details
    Browse the repository at this point in the history

  3. Review

    @xroblot
    xroblot committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    dde1762 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2024

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

    …e_def
    @xroblot
    xroblot committed May 11, 2024
    Configuration menu
    Copy the full SHA
    5bf273f View commit details
    Browse the repository at this point in the history

  2. update

    @xroblot
    xroblot committed May 11, 2024
    Configuration menu
    Copy the full SHA
    32238a3 View commit details
    Browse the repository at this point in the history

  3. More lemmas

    @xroblot
    xroblot committed May 11, 2024
    Configuration menu
    Copy the full SHA
    2af9cd2 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2024

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

    …e_def
    @xroblot
    xroblot committed May 20, 2024
    Configuration menu
    Copy the full SHA
    cf69fd5 View commit details
    Browse the repository at this point in the history

  2. backport changes

    @xroblot
    xroblot committed May 20, 2024
    Configuration menu
    Copy the full SHA
    b535bb7 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2024

  1. 1st commit

    @xroblot
    xroblot committed May 22, 2024
    Configuration menu
    Copy the full SHA
    6b8221e View commit details
    Browse the repository at this point in the history

Commits on May 23, 2024

  1. Add docstring + apply lemmas

    @xroblot
    xroblot committed May 23, 2024
    Configuration menu
    Copy the full SHA
    affe7ce View commit details
    Browse the repository at this point in the history

  2. Merge branch 'xfr_add-normatplace' into xfr_fundamental_cone_def

    @xroblot
    xroblot committed May 23, 2024
    Configuration menu
    Copy the full SHA
    26c98a3 View commit details
    Browse the repository at this point in the history

  3. New version

    @xroblot
    xroblot committed May 23, 2024
    Configuration menu
    Copy the full SHA
    6987779 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2024

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

    …e_def
    @xroblot
    xroblot committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    2567d4c View commit details
    Browse the repository at this point in the history

  2. update

    @xroblot
    xroblot committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    5278abb View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2024

  1. 1st commit

    @xroblot
    xroblot committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    f846a96 View commit details
    Browse the repository at this point in the history

  2. Clean up

    @xroblot
    xroblot committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    912f9be View commit details
    Browse the repository at this point in the history

  3. Docstring

    @xroblot
    xroblot committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    f189562 View commit details
    Browse the repository at this point in the history

  4. Fix lint

    @xroblot
    xroblot committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    0e73e92 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2024

  1. Merge remote-tracking branch 'origin/master' into xfr-zlattices_as_z-… 

    …modules
    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    889d6ac View commit details
    Browse the repository at this point in the history

  2. Typo

    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    a9fda3a View commit details
    Browse the repository at this point in the history

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

    …e_def
    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    c0da1f5 View commit details
    Browse the repository at this point in the history

  4. Fix

    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    37cdc67 View commit details
    Browse the repository at this point in the history

  5. update

    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    b9a1990 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean 

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

  7. clean up

    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    42506d3 View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/xfr-zlattices_as_z-modules' into… 

    … xfr_fundamental_cone_def
    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    0b84773 View commit details
    Browse the repository at this point in the history

  9. fix afer merge

    @xroblot
    xroblot committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    eccfeda View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

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

    …e_def
    @xroblot
    xroblot committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    218dcdb View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2024

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

    …e_def
    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    db630fa View commit details
    Browse the repository at this point in the history

  2. Review

    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    2102bc0 View commit details
    Browse the repository at this point in the history

  3. 1st commit

    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    dd48363 View commit details
    Browse the repository at this point in the history

  4. Deprecated

    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    de353a9 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean 

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

  6. Clean up

    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    676ece8 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'refs/remotes/origin/xfr_fundamental_con… 

    …e_unit_smul' into xfr_fundamental_cone_unit_smul
    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    33037c3 View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/xfr_fundamental_cone_unit_smul' … 

    …into xfr_fundamental_cone_log_map
    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    500e79f View commit details
    Browse the repository at this point in the history

  9. 1st commit

    @xroblot
    xroblot committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    e8e3cbd View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2024

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

    …e_log_map
    @xroblot
    xroblot committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    6bd3c44 View commit details
    Browse the repository at this point in the history

  2. Add some simp

    @xroblot
    xroblot committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    4522225 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2024

  1. Merge remote-tracking branch 'origin/xfr_fundamental_cone_log_map' in… 

    …to xfr_fundamental_cone_def
    @xroblot
    xroblot committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    e44c128 View commit details
    Browse the repository at this point in the history

  2. Duplicate lemma

    @xroblot
    xroblot committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    e8dc7d3 View commit details
    Browse the repository at this point in the history

  3. Update FundamentalCone.lean

    @xroblot
    xroblot authored Sep 16, 2024
    Configuration menu
    Copy the full SHA
    8adedf0 View commit details
    Browse the repository at this point in the history

  4. Update FundamentalCone.lean

    @xroblot
    xroblot authored Sep 16, 2024
    Configuration menu
    Copy the full SHA
    702057c View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Fundamenta… 

    …lCone.lean

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

Commits on Sep 17, 2024

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

    …e_def
    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    12f996d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'refs/remotes/origin/xfr_fundamental_con… 

    …e_def' into xfr_fundamental_cone_def
    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    4199db3 View commit details
    Browse the repository at this point in the history

  3. Update Basic.lean

    @xroblot
    xroblot authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    f53e61a View commit details
    Browse the repository at this point in the history

  4. clean up

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    2252cf4 View commit details
    Browse the repository at this point in the history

  5. Update FundamentalCone.lean

    @xroblot
    xroblot authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    966c177 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Fundamenta… 

    …lCone.lean

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

  7. Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Fundamenta… 

    …lCone.lean

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

  8. Review

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    1a12c46 View commit details
    Browse the repository at this point in the history

  9. rfl

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    3460cc6 View commit details
    Browse the repository at this point in the history

  10. Merge remote-tracking branch 'refs/remotes/origin/xfr_fundamental_con… 

    …e_def' into xfr_fundamental_cone_def
    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    b4a0e68 View commit details
    Browse the repository at this point in the history

  11. fix defeq abuse

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    3467d82 View commit details
    Browse the repository at this point in the history

  12. clean up

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    974b8c5 View commit details
    Browse the repository at this point in the history

  13. more defeq

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    fe7db50 View commit details
    Browse the repository at this point in the history

  14. whitespace

    @xroblot
    xroblot committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    5bb55bc View commit details
    Browse the repository at this point in the history