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

feat(number_theory/number_field/units): prove results about units - #18267

Closed
xroblot wants to merge 314 commits into
masterfrom
xfr-log_emb
Closed

feat(number_theory/number_field/units): prove results about units#18267
xroblot wants to merge 314 commits into
masterfrom
xfr-log_emb

Conversation

@xroblot

@xroblot xroblot commented Jan 23, 2023 •
edited by github-actions Bot
Loading

Copy link
Copy Markdown
Collaborator

xroblot added 30 commits November 30, 2022 11:46
@xroblot
Reuse pi definitions
ff59237
@xroblot
major refactor
fa11b99
@xroblot
Update
e492f3a
@xroblot
Merge remote-tracking branch 'origin/xfr-place_eq' into xfr-complex_p…
bc74c2a 
…laces
@xroblot
Merge
0f3e912
@xroblot
Merge remote-tracking branch 'origin/xfr-pi.monoid_hom' into xfr-clas…
4c341f7 
…sical_emb
@xroblot
WIP
ace41fe
@xroblot
add embeddings
9c2ee97
@xroblot
WIP
f7f78fc
@xroblot
Merge remote-tracking branch 'origin/master' into xfr-place_eq_topo
82f53e4
@xroblot
Merge remote-tracking branch 'origin/xfr-place_eq_topo' into xfr-plac…
e83ade5 
…e_eq
@xroblot
Merge remote-tracking branch 'origin/xfr-place_eq' into xfr-complex_p…
a795a2a 
…laces
@xroblot
Merge remote-tracking branch 'origin/xfr-complex_places' into xfr-cla…
72f661c 
…ssical_emb
@xroblot
WIP
ff2f1b5
@xroblot
Add header (for CI)
fe8df01
@xroblot
Move file
f8cc0df
@xroblot
CI
f4f618f
@xroblot
Fix name & docstring
b270ea4
@xroblot
Merge remote-tracking branch 'origin/xfr-place_eq' into xfr-complex_p…
5c12093 
…laces
@xroblot
Merge remote-tracking branch 'origin/xfr-complex_places' into xfr-cla…
8e69c48 
…ssical_emb
@xroblot
WIP
821affc
@xroblot
WIP
d85c1a6
@xroblot
WIP
1b01d66
@xroblot
WIP
59736c0
@xroblot
Review
d74d5f2
@xroblot
WIP
39d483a
@xroblot
Major name changes
6ad1c09
@xroblot
Remove embeddings.is_complex
e0afdf3
@xroblot
Add namespace complex_embeddings
c597d83
@xroblot
WIP
ca3f1ee
xroblot added 24 commits December 24, 2022 18:20
@xroblot
WIP
71e132c
@xroblot
Add aux lemmas
1d3e178
@xroblot
Merge branch 'xfr-classical_emb' of https://github.com/leanprover-com…
afb89d8 
…munity/mathlib into xfr-log_emb
@xroblot
Add results about roots_of_unity
6ac7f35
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
49a8d56 
 into xfr-log_emb
@xroblot
Add countable
ec953dd
@xroblot
Merge branch 'xfr-classical_emb' of https://github.com/leanprover-com…
8ce495e 
…munity/mathlib into xfr-log_emb
@xroblot
Add inter_ball_finite
979b15f
@xroblot
WIP
ed2f135
@xroblot
Golf
8c0bb15
@xroblot
Merge branch 'xfr-classical_emb' of https://github.com/leanprover-com…
9ef4ba5 
…munity/mathlib into xfr-log_emb
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
04f648e 
 into xfr-log_emb
@xroblot
WIP
3cecc5f
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
6a1af63 
 into xfr-place_eq
@xroblot
Merge branch 'xfr-place_eq' into xfr-complex_places
670749e
@xroblot
Merge branch 'xfr-complex_places' of https://github.com/leanprover-co…
3e6bb98 
…mmunity/mathlib into xfr-classical_emb
@xroblot
Fix import
9aeb468
@xroblot
Merge branch 'xfr-place_eq' of https://github.com/leanprover-communit…
9913e34 
…y/mathlib into xfr-complex_places
@xroblot
Merge branch 'xfr-complex_places' of https://github.com/leanprover-co…
960b01a 
…mmunity/mathlib into xfr-classical_emb
@xroblot
Merge branch 'master' of https://github.com/leanprover-community/mathlib
34c5261 
 into xfr-place_eq
@xroblot
Better names
639df71
@xroblot
Merge branch 'xfr-place_eq' of https://github.com/leanprover-communit…
27c02d2 
…y/mathlib into xfr-complex_places
@xroblot
Merge branch 'xfr-complex_places' of https://github.com/leanprover-co…
888ffcd 
…mmunity/mathlib into xfr-classical_emb
@xroblot
Merge branch 'xfr-classical_emb' of https://github.com/leanprover-com…
7de4a5d 
…munity/mathlib into xfr-log_emb
@xroblot xroblot added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jan 23, 2023
@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 Jan 23, 2023
@ghost

ghost commented Jan 23, 2023

Copy link
Copy Markdown

This PR/issue depends on:

@xroblot xroblot closed this Jan 24, 2023
@xroblot
xroblot deleted the xfr-log_emb branch January 24, 2023 07:54
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

blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@xroblot @ADedecker