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.FLT.Three): add various results #14119

Closed
wants to merge 17 commits into from
Closed

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

wants to merge 17 commits into from

Conversation

riccardobrasca
Copy link
Member

@riccardobrasca riccardobrasca commented Jun 25, 2024 •
edited
Loading

We add various results needed to prove flt3.

From the flt3 project at LFTCM2024.

Open in Gitpod

@github-actions GitHub Actions
Copy link

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

PR summary 62160a2859

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.NumberTheory.FLT.Three 2125 2132 +7 (+0.33%)

Declarations diff

+ Solution'.two_le_multiplicity
+ Solution.two_le_multiplicity
+ _root_.IsPrimitiveRoot.toInteger_cube_eq_one
+ a_cube_add_b_cube_eq_mul
+ a_cube_b_cube_congr_one_or_neg_one
+ ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd
+ exists_Solution_of_Solution'
+ lambda_pow_four_dvd_c_cube
+ lambda_sq_dvd_c
+ lambda_sq_dvd_or_dvd_or_dvd
+ toInteger_sub_one_not_dvd_two

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 changed the title add toInteger_sub_one_not_dvd_two feat(Mathlib.NumberTheory.FLT.Three): add various results Jun 25, 2024
@riccardobrasca riccardobrasca added awaiting-review t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebra Algebra (groups, rings, fields, etc) labels Jun 25, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Jun 26, 2024
View reviewed changes
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 26, 2024
riccardobrasca and others added 8 commits June 26, 2024 12:23
@riccardobrasca riccardobrasca added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 26, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 27, 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

maintainer merge

@github-actions GitHub Actions
Copy link

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

jcommelin
jcommelin reviewed Jun 28, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 28, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 28, 2024
@riccardobrasca
feat(Mathlib.NumberTheory.FLT.Three): add various results (#14119)
81d1026 
We add various results needed to prove flt3.

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

mathlib-bors bot commented Jun 28, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Mathlib.NumberTheory.FLT.Three): add various results [Merged by Bors] - feat(Mathlib.NumberTheory.FLT.Three): add various results Jun 28, 2024
@mathlib-bors mathlib-bors bot closed this Jun 28, 2024
@mathlib-bors mathlib-bors bot deleted the RB/almost_flt3 branch June 28, 2024 11:41
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@riccardobrasca @dagurtomas
feat(Mathlib.NumberTheory.FLT.Three): add various results (#14119)
c762a34 
We add various results 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

@jcommelin jcommelin jcommelin left review comments

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

Assignees
No one assigned
Labels
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.
4 participants
@riccardobrasca @jcommelin @Ruben-VandeVelde @leanprover-community-mathlib4-bot