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: cyclotomic fields are totally complex #10502

Closed

riccardobrasca wants to merge 19 commits into master from RB/totally_complex

Member

riccardobrasca commented Feb 13, 2024 •

edited

We prove that cyclotomic fields are totally complex.

From flt-regular.

riccardobrasca added awaiting-review t-number-theory t-algebra labels

riccardobrasca requested a review from xroblot

February 13, 2024 16:47

github-actions bot reviewed

View reviewed changes

Mathlib/NumberTheory/NumberField/Embeddings.lean Outdated Show resolved Hide resolved

riccardobrasca mentioned this pull request

feat: the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5 #10540

Closed

2 tasks

xroblot approved these changes

View reviewed changes

Mathlib/NumberTheory/NumberField/Embeddings.lean Show resolved Hide resolved

Mathlib/NumberTheory/NumberField/Embeddings.lean Show resolved Hide resolved

Member Author

riccardobrasca commented Feb 14, 2024

@xroblot Do you see a quick way of proving that if finrank K = 1 then NrRealPlaces K = 1?

Collaborator

xroblot commented Feb 14, 2024

@xroblot Do you see a quick way of proving that if finrank K = 1 then NrRealPlaces K = 1?

Well, I don't see a better way than to use NumberField.InfinitePlace.card_add_two_mul_card_eq_rank but I am sure you know that already.

Well, there might something possible using: IsUnramifiedAtInfinitePlaces_of_odd_finrank. It could be a bit faster... I am not sure.

Member Author

riccardobrasca commented Feb 14, 2024

@xroblot Do you see a quick way of proving that if finrank K = 1 then NrRealPlaces K = 1?

Well, I don't see a better way than to use NumberField.InfinitePlace.card_add_two_mul_card_eq_rank but I am sure you know that already.

Well, there might something possible using: IsUnramifiedAtInfinitePlaces_of_odd_finrank. It could be a bit faster... I am not sure.

Ah, you're right! I didn't realize that NumberField.InfinitePlace.card_add_two_mul_card_eq_rank immediately gives a + 2*b = 1 so a = 1 and b = 0!

Member Author

riccardobrasca commented Feb 14, 2024

I've generalized the fact that NrComplexPlaces K = φ n / 2 without the assumption that 2 < n (of course it holds for stupid reasons, but still).

riccardobrasca force-pushed the RB/totally_complex branch from d4c66e2 to d409679 Compare

February 18, 2024 11:11

This was referenced Feb 18, 2024

feat: the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5 #10682

Closed

[Merged by Bors] - feat: the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5 #10683

Closed

leanprover-community-mathlib4-bot added the merge-conflict label

riccardobrasca force-pushed the RB/totally_complex branch from ec7b5ed to 8a9eeea Compare

February 19, 2024 15:10

riccardobrasca and others added 14 commits

February 19, 2024 16:14


          feat: cyclotomic fields are totally complex

cb791c7

ops

6c8ad45


          add nrRealPlaces_eq_zero_of_two_lt

291e777


          Update Mathlib/NumberTheory/NumberField/Embeddings.lean

7a560bb

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>


          golf

56ac24a


          fix import

46652a4

ops

5a6b67b


          this is more general

75e9cc1

doc

bbdd32e


          better statement

c7c7603


          useless

e672973


          golf

75d0fda


          add nrRealPlaces_eq_one_of_finrank_eq_one

9e9d2a0


          generalize nrComplexPlaces_eq_totient_div_two

80b3d48


          make a variable explicit

53dad3f

riccardobrasca force-pushed the RB/totally_complex branch from 8a9eeea to 53dad3f Compare

February 19, 2024 15:15

leanprover-community-mathlib4-bot removed the merge-conflict label

faenuccio reviewed

View reviewed changes

Mathlib/NumberTheory/Cyclotomic/Embeddings.lean Outdated Show resolved Hide resolved

faenuccio reviewed

View reviewed changes

Mathlib/NumberTheory/NumberField/Embeddings.lean Outdated Show resolved Hide resolved

Collaborator

faenuccio commented Feb 27, 2024

Besides the two golfing, LGTM.

riccardobrasca and others added 4 commits

February 27, 2024 13:47


          golf

a71364f


          Update Mathlib/NumberTheory/Cyclotomic/Embeddings.lean

42bb25f

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>


          add doc

2960b70


          Merge branch 'master' into RB/totally_complex

cd3cdb0

Member

jcommelin commented Mar 1, 2024

Thanks 🎉

bors merge

github-actions bot added ready-to-merge and removed awaiting-review labels

mathlib-bors bot pushed a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

267bced

We prove that cyclotomic fields are totally complex.

From flt-regular.

mathlib-bors bot commented Mar 1, 2024

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat: cyclotomic fields are totally complex~~ [Merged by Bors] - feat: cyclotomic fields are totally complex

mathlib-bors bot closed this

mathlib-bors bot deleted the RB/totally_complex branch

March 1, 2024 15:31

riccardobrasca added a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

6993b68

We prove that cyclotomic fields are totally complex.

From flt-regular.

mathlib-bors bot pushed a commit that referenced this pull request


          feat: the ring of integers of the p-th cyclotomic field is a PID if p…

5f834b3

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

kbuzzard pushed a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

76350cb

We prove that cyclotomic fields are totally complex.

From flt-regular.

kbuzzard pushed a commit that referenced this pull request


          feat: the ring of integers of the p-th cyclotomic field is a PID if p…

c3a7f33

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

dagurtomas pushed a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

05c41d4

We prove that cyclotomic fields are totally complex.

From flt-regular.

dagurtomas pushed a commit that referenced this pull request


          feat: the ring of integers of the p-th cyclotomic field is a PID if p…

6d32016

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

utensil pushed a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

340df02

We prove that cyclotomic fields are totally complex.

From flt-regular.

utensil pushed a commit that referenced this pull request


          feat: the ring of integers of the p-th cyclotomic field is a PID if p…

9c7d843

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

Louddy pushed a commit that referenced this pull request


          feat: cyclotomic fields are totally complex (#10502)

4b08bca

We prove that cyclotomic fields are totally complex.

From flt-regular.

Louddy pushed a commit that referenced this pull request


          feat: the ring of integers of the p-th cyclotomic field is a PID if p…

f34cf3b

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

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