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(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem #5960

Closed
wants to merge 104 commits into from
Closed

[Merged by Bors] - feat(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem #5960

wants to merge 104 commits into from

Commits on Jun 27, 2023

  1. First version

    @xroblot
    xroblot committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    6079e9f View commit details
    Browse the repository at this point in the history

  2. Remove unneeded instance

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

Commits on Jun 28, 2023

  1. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    f36170f View commit details
    Browse the repository at this point in the history

  2. Add mem_span_integralBasis

    @xroblot
    xroblot committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    a32c2fc View commit details
    Browse the repository at this point in the history

  3. Add apply_mem_span_image_iff_mem_span

    @xroblot
    xroblot committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    3695a30 View commit details
    Browse the repository at this point in the history

  4. Add mem_span_latticeBasis

    @xroblot
    xroblot committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    45552e8 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. Small golf

    @xroblot
    xroblot committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    b34f464 View commit details
    Browse the repository at this point in the history

  2. Add conj_apply

    @xroblot
    xroblot committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    c6c9ddb View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2023

  1. 1st commit

    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    a8f9677 View commit details
    Browse the repository at this point in the history

  2. Fix line

    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    0695983 View commit details
    Browse the repository at this point in the history

  3. merge

    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    c92dd54 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    7b564c8 View commit details
    Browse the repository at this point in the history

  5. merge

    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    91e8c78 View commit details
    Browse the repository at this point in the history

  6. Fix backport

    @xroblot
    xroblot committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    047b8c9 View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2023

  1. Move instance

    @xroblot
    xroblot committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    00c63dc View commit details
    Browse the repository at this point in the history

  2. 1st commit

    @xroblot
    xroblot committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    00a9038 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'xfr-countable_span' into xfr-canonical_embedding_minkowski

    @xroblot
    xroblot committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    d9ec7f1 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2023

  1. 1st commit

    @xroblot
    xroblot committed Jul 5, 2023
    Configuration menu
    Copy the full SHA
    7ef7609 View commit details
    Browse the repository at this point in the history

  2. Add Group.fg_iff_Subgroup_fg

    @xroblot
    xroblot committed Jul 5, 2023
    Configuration menu
    Copy the full SHA
    3a56308 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2023

  1. semicolon

    @xroblot
    xroblot committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    fa22093 View commit details
    Browse the repository at this point in the history

  2. 1st commit

    @xroblot
    xroblot committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    de183ff View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2023

  1. add results about rootsOfUnity

    @xroblot
    xroblot committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    993f95a View commit details
    Browse the repository at this point in the history

  2. Update Zlattice.lean

    @xroblot
    xroblot committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    21d7345 View commit details
    Browse the repository at this point in the history

  3. Update Zlattice.lean

    @xroblot
    xroblot committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    eb432f7 View commit details
    Browse the repository at this point in the history

  4. Update Zlattice.lean

    @xroblot
    xroblot committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    1a266f6 View commit details
    Browse the repository at this point in the history

  5. Update Zlattice.lean

    @xroblot
    xroblot committed Jul 8, 2023
    Configuration menu
    Copy the full SHA
    95d2fcd View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2023

  1. 1st commit

    @xroblot
    xroblot committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    f999e2e View commit details
    Browse the repository at this point in the history

  2. Update

    @xroblot
    xroblot committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    07325e1 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'xfr-countable_span' into xfr-dirichlet

    @xroblot
    xroblot committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    992499e View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. Update

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    55b67ea View commit details
    Browse the repository at this point in the history

  2. Merge branch 'xfr-zlattice_main' into xfr-dirichlet

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    c0c771d View commit details
    Browse the repository at this point in the history

  3. minimize imports

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    d715893 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    ac06af4 View commit details
    Browse the repository at this point in the history

  5. update

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    892e300 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin' into xfr-unit-torsion

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    2337643 View commit details
    Browse the repository at this point in the history

  7. Update

    @xroblot
    xroblot committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    4a13f86 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2023

  1. Merge branch 'xfr-refactor_canonical_embedding', remote-tracking bran… 

    …ch 'origin' into xfr-canonical_embedding_minkowski
    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    584fc5e View commit details
    Browse the repository at this point in the history

  2. Update

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    b33d146 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin' into xfr-zlattice_main

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    e369851 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/xfr-zlattice_main' into xfr-zlat… 

    …tice_main
    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    b9dc461 View commit details
    Browse the repository at this point in the history

  5. More semicolons

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    bc27220 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'xfr-unit-torsion' into xfr-dirichlet

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    045cb4a View commit details
    Browse the repository at this point in the history

  7. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    6395d1c View commit details
    Browse the repository at this point in the history

  8. backport

    @xroblot
    xroblot committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    18d3d61 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    a289ca4 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. 1st commit

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

Commits on Jul 28, 2023

  1. Merge branch 'xfr-refactor_embeddings' into xfr-refactor_canonical_em… 

    …bedding
    @xroblot
    xroblot committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    f83eda3 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em… 

    …bedding_minkowski
    @xroblot
    xroblot committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    0eb1f7f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

    @xroblot
    xroblot committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    1102702 View commit details
    Browse the repository at this point in the history

Commits on Aug 3, 2023

  1. Merge remote-tracking branch 'origin' into xfr-zlattice_main

    @xroblot
    xroblot committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    0d22cb8 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    e794a35 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em… 

    …bedding_minkowski
    @xroblot
    xroblot committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    57728b0 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    b8bb31d View commit details
    Browse the repository at this point in the history

  5. Fix align_import

    @xroblot
    xroblot committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    fd620f4 View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2023

  1. add Finite_bounded_inter_isClosed

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

  2. Switch to DiscreteTopology

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

  3. Merge branch 'xfr-refactor_canonical_embedding' into xfr-canonical_em… 

    …bedding_minkowski
    @xroblot
    xroblot committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    e1bec08 View commit details
    Browse the repository at this point in the history

  4. Line too long

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

  5. Merge branch 'xfr-zlattice_main' into xfr-canonical_embedding_minkowski

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

  6. merge

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

  7. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

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

Commits on Aug 8, 2023

  1. Merge remote-tracking branch 'origin' into xfr-dirichlet

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

  2. add main statements

    @xroblot
    xroblot committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    3dc3436 View commit details
    Browse the repository at this point in the history

  3. 1st commit

    @xroblot
    xroblot committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    01e244b View commit details
    Browse the repository at this point in the history

  4. Add docs

    @xroblot
    xroblot committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    6324f71 View commit details
    Browse the repository at this point in the history

  5. Add QuotientGroup.mk_prod

    @xroblot
    xroblot committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    6f2f39b View commit details
    Browse the repository at this point in the history

  6. Fix statement

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

  7. Use DiscreteTopology

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

  8. Fix docs

    @xroblot
    xroblot committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    4114da1 View commit details
    Browse the repository at this point in the history

  9. More fixes

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

Commits on Aug 9, 2023

  1. Add the proof of Gershgorin

    @xroblot
    xroblot committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    44a095d View commit details
    Browse the repository at this point in the history

  2. review

    @xroblot
    xroblot committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    b20a260 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'xfr-matrix_det_lemma' into xfr-dirichlet

    @xroblot
    xroblot committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    b937109 View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2023

  1. Merge

    @xroblot
    xroblot committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    2169056 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into xfr-refactor_canonical_emb… 

    …edding
    @xroblot
    xroblot committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    f0f6cbb View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2023

  1. Docstrings

    @xroblot
    xroblot committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    bf2b10e View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/xfr-refactor_canonical_embedding… 

    …' into xfr-canonical_embedding_minkowski
    @xroblot
    xroblot committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    891be93 View commit details
    Browse the repository at this point in the history

  3. Docstring

    @xroblot
    xroblot committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    30681d1 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2023

  1. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Aug 19, 2023
    Configuration menu
    Copy the full SHA
    02a0d54 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

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

Commits on Aug 20, 2023

  1. fix names

    @xroblot
    xroblot committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    62c5985 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Aug 20, 2023
    Configuration menu
    Copy the full SHA
    ef355cd View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2023

  1. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    c7bfae6 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2023

  1. typo

    @xroblot
    xroblot committed Aug 25, 2023
    Configuration menu
    Copy the full SHA
    f0076cf View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2023

  1. 1st commit

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

  2. Merge branch 'xfr_complex_measure_ishaar' into xfr-canonical_embeddin… 

    …g_minkowski
    @xroblot
    xroblot committed Aug 28, 2023
    Configuration menu
    Copy the full SHA
    a31dacd View commit details
    Browse the repository at this point in the history

  3. Cleanup

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

  4. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

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

  5. Merge

    @xroblot
    xroblot committed Aug 28, 2023
    Configuration menu
    Copy the full SHA
    809f8f1 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2023

  1. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Sep 1, 2023
    Configuration menu
    Copy the full SHA
    7e09f65 View commit details
    Browse the repository at this point in the history

  2. Backport

    @xroblot
    xroblot committed Sep 1, 2023
    Configuration menu
    Copy the full SHA
    3bd156c View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2023

  1. Merge remote-tracking branch 'origin' into xfr-canonical_embedding_mi… 

    …nkowski
    @xroblot
    xroblot committed Sep 16, 2023
    Configuration menu
    Copy the full SHA
    629f33b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'xfr-canonical_embedding_minkowski' into xfr-dirichlet

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

  3. Clean up after merge

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

  4. Update Mathlib/NumberTheory/NumberField/Units.lean 

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

Commits on Sep 20, 2023

  1. Merge remote-tracking branch 'origin' into xfr-dirichlet

    @xroblot
    xroblot committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    3488aff View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2023

  1. Clean up after merge

    @xroblot
    xroblot committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    b786b22 View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2023

  1. Review

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

Commits on Sep 23, 2023

  1. Fix docstrings

    @xroblot
    xroblot committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    872d1e0 View commit details
    Browse the repository at this point in the history

  2. new section

    @xroblot
    xroblot committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    ae68a0a View commit details
    Browse the repository at this point in the history

  3. Long line

    @xroblot
    xroblot committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    1020c10 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2023

  1. Review

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

  2. whitespace

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

  3. Review

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