Skip to content

[Merged by Bors] - feat: Polynomial FLT#18882

Closed
seewoo5 wants to merge 46 commits intomasterfrom
feature/poly-flt
Closed

[Merged by Bors] - feat: Polynomial FLT#18882
seewoo5 wants to merge 46 commits intomasterfrom
feature/poly-flt

Conversation

@seewoo5
Copy link
Copy Markdown
Collaborator

@seewoo5 seewoo5 commented Nov 11, 2024 •
edited by YaelDillies
Loading

Prove the polynomial FLT, using Mason-Stothers theorem #15706. More generally, prove non-solvability of Fermat-Catalan equation: $ux^p + vx^q + wz^r = 0$ where $u, v, w \in k^\times$ are units and $p, q, r \ge 3$ with $pq + qr + rp \le pqr$.

Also derive the IsCoprime b c and IsCoprime c a assumptions from the IsCoprime a b and a + b + c = 0 ones in Polynomial.abc.

Open in Gitpod

@seewoo5 seewoo5 added the t-algebra Algebra (groups, rings, fields, etc) label Nov 11, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 11, 2024 •
edited
Loading

PR summary 31b1f512b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.FLT.Polynomial (new file) 1190

Declarations diff

+ Polynomial.flt
+ Polynomial.flt_catalan
+ fermatLastTheoremWith'_polynomial

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Nov 11, 2024
@seewoo5
Copy link
Copy Markdown
Collaborator Author

seewoo5 commented Nov 12, 2024

@jcpaik Could you help me to remove sorrys? Also, flt_catalan_aux haven't fixed yet.

jcpaik and others added 6 commits November 14, 2024 11:12
@jcpaik
write Polynomial.abc not abc
a0fd1f5
@jcpaik
rename lemmas
7ef441c
@jcpaik
progress on catalan_deriv
2dde7da
@jcpaik
complete flt-deriv lemma
c55272f
@jcpaik @github-actions
lint
48b3f87 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jcpaik @github-actions
lint
626b843 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jcpaik jcpaik mentioned this pull request Nov 14, 2024
Merged
@jcpaik jcpaik mentioned this pull request Nov 14, 2024
Merged
jcpaik and others added 3 commits November 15, 2024 01:05
@jcpaik @github-actions
lint
772ac1c 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jcpaik @github-actions
lint
1006aad 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jcpaik @github-actions
lint
579caab 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jcpaik
Copy link
Copy Markdown
Collaborator

jcpaik commented Nov 14, 2024

@jcpaik Could you help me to remove sorrys? Also, flt_catalan_aux haven't fixed yet.

Merge the PRs then the file is sorry-free and proves polynomial FLT. We only then need to golf/separate the file into smaller pieces.

@seewoo5 seewoo5 mentioned this pull request Nov 15, 2024
Closed
@seewoo5 seewoo5 mentioned this pull request Jan 4, 2025
Closed
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 4, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jan 4, 2025

This PR/issue depends on:

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 4, 2025
@seewoo5 seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 5, 2025
YaelDillies
YaelDillies reviewed Jan 5, 2025
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 5, 2025
seewoo5 and others added 2 commits January 6, 2025 14:27
@seewoo5 @YaelDillies
Apply suggestions from code review
c6c91f4 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@seewoo5
update doc
5e427a5
@seewoo5 seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 6, 2025
YaelDillies
YaelDillies reviewed Jan 6, 2025
View reviewed changes
@jcpaik @YaelDillies
English grammar
df4efef 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jan 6, 2025 •
edited
Loading

Looks good to me! @kbuzzard ?

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 6, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 6, 2025
kbuzzard
kbuzzard approved these changes Jan 6, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

A couple more docstring nits. Thanks a lot!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2025

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 6, 2025
@seewoo5 @kbuzzard
Update docs
31b1f51 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@seewoo5
Copy link
Copy Markdown
Collaborator Author

seewoo5 commented Jan 6, 2025

Thank you all!

bors r+

@seewoo5 seewoo5 mentioned this pull request Jan 6, 2025
Closed
5 tasks
mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025
@seewoo5 @jcpaik
feat: Polynomial FLT (#18882)
ee71c31 
Prove the polynomial FLT, using Mason-Stothers theorem #15706. More generally, prove non-solvability of Fermat-Catalan equation: $ux^p + vx^q + wz^r = 0$ where $u, v, w \in k^\times$ are units and $p, q, r \ge 3$ with $pq + qr + rp \le pqr$.

Also derive the `IsCoprime b c` and `IsCoprime c a` assumptions from the `IsCoprime a b` and `a + b + c = 0` ones in  `Polynomial.abc`.



Co-authored-by: Jineon Baek <jineon@umich.edu>
Co-authored-by: Jineon Baek <34874130+jcpaik@users.noreply.github.com>
Co-authored-by: Seewoo Lee <seewoo5@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Polynomial FLT [Merged by Bors] - feat: Polynomial FLT Jan 6, 2025
@mathlib-bors mathlib-bors bot closed this Jan 6, 2025
@mathlib-bors mathlib-bors bot deleted the feature/poly-flt branch January 6, 2025 16:44
Julian added a commit that referenced this pull request Jan 6, 2025
@Julian
Merge remote-tracking branch 'origin/master' into nat-ideal-eq-top
ca07f7f 
* origin/master: (189 commits)
  chore(Algebra): make more names consistent (#20449)
  feat: Polynomial FLT (#18882)
  feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457)
  fix: linkfix in 100.yaml (#20517)
  feat(1000): fill in more entries (#20470)
  feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769)
  feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462)
  feat(RingTheory): classification of etale algebras over fields (#20324)
  fix: Allow multiple builds on staging branch (#20515)
  feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337)
  chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863)
  chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514)
  refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474)
  feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)
  chore(RingTheory/Finiteness): rename Module.Finite.out (#20506)
  refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508)
  feat(CategoryTheory): products in the category of Ind-objects (#20507)
  chore: remove >9 month old deprecations (#20505)
  chore(FieldTheory/Galois): small cleanup (#20217)
  chore(LinearIndependent): generalize to semirings (#20480)
  chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500)
  chore: replace `aesop` with `simp` where possible (#20483)
  chore(1000): remove nonexistent fields (#20493)
  chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490)
  feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458)
  feat: a conditional kernel is almost everywhere a probability measure (#20430)
  feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304)
  feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479)
  chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492)
  feat(FaaDiBruno): derive `DecidableEq` (#20482)
  chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413)
  chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351)
  chore(MvPolynomial/Localization): golf using TensorProduct (#20309)
  chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277)
  chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259)
  feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091)
  fix: Stop cancelling builds of master (#20435)
  chore: update Mathlib dependencies 2025-01-05 (#20485)
  feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)
  chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
  chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
  feat: shorthand lemmas for the L1 norm (#20383)
  chore: remove unnecessary adaptation notes (#20467)
  chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473)
  chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888)
  feat(Algebra): more on `OrthogonalIdempotents` (#18195)
  feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468)
  feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190)
  feat(Algebra/Lie): add Lie's theorem (#13480)
  chore(RingTheory/Generators): make algebra instance a def (#14265)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tb65536 tb65536 tb65536 left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@kbuzzard kbuzzard kbuzzard approved these changes

+1 more reviewer

@jcpaik jcpaik jcpaik left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@jcpaik jcpaik

@seewoo5 seewoo5

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! 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.

7 participants

@seewoo5 @jcpaik @YaelDillies @mathlib4-dependent-issues-bot @tb65536 @kbuzzard @leanprover-community-bot-assistant