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

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

Closed
riccardobrasca opened this issue Feb 22, 2023 · 1 comment
Closed

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

riccardobrasca opened this issue Feb 22, 2023 · 1 comment
Assignees
@xroblot
Labels
t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Comments

@riccardobrasca
Copy link
Member

No description provided.

@leanprover-community leanprover-community locked and limited conversation to collaborators Feb 22, 2023
@leanprover-community leanprover-community unlocked this conversation Feb 22, 2023
@xroblot xroblot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Feb 23, 2023
This was linked to pull requests Feb 23, 2023
[Merged by Bors] - feat(algebra/module/zlattice): prove some results about Z-lattices #18266
Closed
[Merged by Bors] - feat(number_theory/number_field/embeddings): some additional lemmas #18473
Closed
feat(number_theory/number_field/unit): proof of Dirichlet's unit theorem #18478
Closed
This was unlinked from pull requests Feb 24, 2023
[Merged by Bors] - feat(algebra/module/zlattice): prove some results about Z-lattices #18266
Closed
[Merged by Bors] - feat(number_theory/number_field/embeddings): some additional lemmas #18473
Closed
@riccardobrasca
Copy link
Member Author

This is now done in mathlib4.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@xroblot xroblot

Labels
t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
2 participants
@riccardobrasca @xroblot