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(Mathlib.NumberTheory.Cyclotomic.Three): add various results #13798

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results #13798

wants to merge 33 commits into from

Conversation

riccardobrasca
Copy link
Member

@riccardobrasca riccardobrasca commented Jun 13, 2024 •
edited
Loading

We add various results about the third cyclotomic field needed to prove flt3.

From the flt3 project at LFTCM2024.

Open in Gitpod

@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 13, 2024 •
edited
Loading

PR summary f68c15cbae

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.Fintype 715 797 +82 (+11.47%)
Mathlib.NumberTheory.Cyclotomic.Three 2128 2129 +1 (+0.05%)

Declarations diff

+ Finset.univ_of_card_le_three
+ Finset.univ_of_card_le_two
+ card_quotient_toInteger_sub_one
+ charP_of_card_eq_prime
+ coe_eta
+ coe_toInteger
+ cube_sub_one_eq_mul
+ eta_sq_add_eta_add_one
+ finite_quotient_toInteger_sub_one
+ lambda_dvd_mul_sub_one_mul_sub_eta_add_one
+ lambda_dvd_or_dvd_sub_one_or_dvd_add_one
+ lambda_pow_four_dvd_cube_add_one_of_dvd_add_one
+ lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one
+ lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
+ ringEquivOfPrime
+ ringEquivOfPrime_eq_ringEquiv

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@riccardobrasca riccardobrasca added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) labels Jun 13, 2024
github-actions[bot]
github-actions bot reviewed Jun 13, 2024
View reviewed changes
riccardobrasca and others added 2 commits June 13, 2024 13:47
@riccardobrasca @github-actions
Update Mathlib/NumberTheory/Cyclotomic/Rat.lean
403721c 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@riccardobrasca @github-actions
Update Mathlib/NumberTheory/Cyclotomic/Rat.lean
80a7a52 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@riccardobrasca riccardobrasca changed the title RB/flt_lemmas feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results Jun 13, 2024
@riccardobrasca riccardobrasca added awaiting-review and removed WIP Work in progress labels Jun 13, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Jun 16, 2024
View reviewed changes
@MichaelStollBayreuth MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 17, 2024
@riccardobrasca riccardobrasca added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 18, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 23, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lgtm, thanks!

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

Vierkantor
Vierkantor reviewed Jun 25, 2024
View reviewed changes
Mathlib/NumberTheory/Cyclotomic/Three.lean
Comment on lines +158 to +163
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
· exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _
· exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _
· refine dvd_mul_of_dvd_right ?_ _
rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]
exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

More note to self than anything to do in this PR: I feel like this should be aesopable...

Vierkantor
Vierkantor approved these changes Jun 25, 2024
View reviewed changes
Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM with Johan's comment, thanks!

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@riccardobrasca
Copy link
Member Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 25, 2024
@riccardobrasca
feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798
5bdfd1a 
)

We add various results about the third cyclotomic field needed to prove flt3.

From the flt3 project at LFTCM2024.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results [Merged by Bors] - feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results Jun 25, 2024
@mathlib-bors mathlib-bors bot closed this Jun 25, 2024
@mathlib-bors mathlib-bors bot deleted the RB/flt_lemmas branch June 25, 2024 10:35
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@riccardobrasca @kbuzzard
feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798
05f356a 
)

We add various results about the third cyclotomic field needed to prove flt3.

From the flt3 project at LFTCM2024.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@riccardobrasca @dagurtomas
feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798
93efefb 
)

We add various results about the third cyclotomic field needed to prove flt3.

From the flt3 project at LFTCM2024.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@jcommelin jcommelin jcommelin left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

@faenuccio faenuccio faenuccio left review comments

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees
No one assigned
Labels
delegated maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
8 participants
@riccardobrasca @TwoFX @Vierkantor @jcommelin @faenuccio @Ruben-VandeVelde @MichaelStollBayreuth @leanprover-community-mathlib4-bot