Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(number_theory/number_field/unit): proof of Dirichlet's unit theorem - #18478

Closed
xroblot wants to merge 808 commits into
masterfrom
xfr-dirichlet
Closed

feat(number_theory/number_field/unit): proof of Dirichlet's unit theorem#18478
xroblot wants to merge 808 commits into
masterfrom
xfr-dirichlet

Conversation

@xroblot

@xroblot xroblot commented Feb 21, 2023 •
edited by github-actions Bot
Loading

Copy link
Copy Markdown
Collaborator

@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 21, 2023
@xroblot xroblot added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Feb 21, 2023
@xroblot xroblot changed the title feat(number_theory/number_field/unit) feat(number_theory/number_field/unit): add Dirichlet's unit theorem Feb 22, 2023
@xroblot xroblot changed the title feat(number_theory/number_field/unit): add Dirichlet's unit theorem feat(number_theory/number_field/unit): proof of Dirichlet's unit theorem Feb 22, 2023
@xroblot xroblot linked an issue Feb 24, 2023 that may be closed by this pull request
Proof that the unit group of a number field is finitely-generated #18482
Closed
xroblot and others added 24 commits March 2, 2023 13:27
@xroblot
Initial commit
ee0aac0
@xroblot
Add docstrings
1de02db
@xroblot
Add is_integral_closure lemmas
3e7a1b9
@xroblot
Review
938e158
@xroblot @Vierkantor
Update src/number_theory/number_field/basic.lean
0e4d057 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@xroblot
1rst commit
7460443
@xroblot
Add int.cast_is_unit_iff
6c458fb
@xroblot
Clean up
6d93e31
@xroblot
add is_integral_closure.module_free
b2bbc69
@xroblot
Better is_domain inference
0b3e1c4
@xroblot
Add is_integral_closure.is_localization
0b3f691
@xroblot
add is_integral_closure.rank
0ae121d
@xroblot
Typo
b546fdd
@xroblot
Merge branch 'xfr_integral_basis' of https://github.com/leanprover-co…
27c97d5 
…mmunity/mathlib into xfr-canonical_embedding
@xroblot
WIP
3fe6c44
@xroblot
Review
c4fa8e5
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
8f5467a 
 into xfr-zlattices
@xroblot
Generalize some results
e2dd3ee
@xroblot
Add comment back
0228996
@xroblot
More generalization
18d380c
@xroblot
WIP
92706b6
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
97969d2 
 into xfr-classical_emb
@xroblot
Define E
e58b21e
@xroblot
WIP
50f8526
xroblot added 23 commits May 5, 2023 21:22
@xroblot
Merge branch 'xfr-zlattices' of https://github.com/leanprover-communi…
fdff3da 
…ty/mathlib into xfr-zlattice_theory
@xroblot
Merge branch 'xfr-zlattice_theory' of https://github.com/leanprover-c…
0d7d6d8 
…ommunity/mathlib into xfr-canonical_embedding
@xroblot
Fix name change
974b433
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
89258af 
 into xfr-unit
@xroblot
Merge branch 'xfr-unit' of https://github.com/leanprover-community/ma…
a831210 
…thlib into xfr-dirichlet
@xroblot
Merge branch 'xfr-canonical_embedding' of https://github.com/leanprov…
f20c665 
…er-community/mathlib into xfr-dirichlet
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
7acd425 
 into xfr-zlattices
@xroblot
Merge branch 'xfr-zlattices' of https://github.com/leanprover-communi…
5992c34 
…ty/mathlib into xfr-zlattice_theory
@xroblot
Merge branch 'xfr-zlattice_theory' of https://github.com/leanprover-c…
be387dd 
…ommunity/mathlib into xfr-canonical_embedding
@xroblot
Merge branch 'xfr-canonical_embedding' of https://github.com/leanprov…
7f0169e 
…er-community/mathlib into xfr-dirichlet
@xroblot
Fix import
a24e1f4
@xroblot
Merge branch 'xfr-zlattices' of https://github.com/leanprover-communi…
b025604 
…ty/mathlib into xfr-zlattice_theory

Fix imports
@xroblot
Use volume
5713fe4 
Use open
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
3e72980 
 into xfr-canonical_embedding
@xroblot
Add instance
61af5bf
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
3b9b9e8 
 into xfr-canonical_embedding
@xroblot
move instance
5f49b1c
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
dfe6edb 
 into xfr-zlattices
@xroblot
Removed locale classical
90caec2
@xroblot
Merge branch 'xfr-zlattices' of https://github.com/leanprover-communi…
60e6c48 
…ty/mathlib into xfr-zlattice_theory
@xroblot
Fix after merge
4228447
@xroblot
Merge branch 'xfr-zlattice_theory' of https://github.com/leanprover-c…
dad701b 
…ommunity/mathlib into xfr-canonical_embedding
@xroblot
Merge branch 'xfr-canonical_embedding' of https://github.com/leanprov…
65e54a7 
…er-community/mathlib into xfr-dirichlet
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 6, 2023
@ghost

ghost commented Jul 6, 2023

Copy link
Copy Markdown

This PR/issue depends on:

@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@xroblot

xroblot commented Jul 16, 2023 •
edited by YaelDillies
Loading

Copy link
Copy Markdown
Collaborator Author

This PR is being ported directly (by hand) to Mathlib4

@xroblot xroblot closed this Jul 16, 2023
@YaelDillies
YaelDillies deleted the xfr-dirichlet branch November 18, 2023 11:25
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Proof that the unit group of a number field is finitely-generated

5 participants

@xroblot @kim-em @eric-wieser @hrmacbeth @urkud