feat: Mason-Stothers theorem (polynomial ABC) #15706

seewoo5 · 2024-08-11T21:50:26Z

Almost last part of porting project of the formalization of polynomial ABC.
This file proves Mason-Stothers theorem (i.e. polynomial ABC). For coprime polynomials $a, b, c$ over a field (of arbitrary characteristic) with $a + b + c = 0$, we have $\max{\deg(a), \deg(b), \deg(c)} + 1 \le \deg(\mathrm{rad}(abc))$ or $a' = b' = c' = 0$.

TODO: After #14720 is merged, add polynomial FLT as a corollary. It is already in here.

depends on: [Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid #14873
depends on: [Merged by Bors] - feat(RingTheory/Radical): Theorems for coprime elements + alpha #15331
depends on: divRadical for polynomials #18452
depends on: feat: IsCoprime.wronskian_eq_zero_iff #18483
Related: [Merged by Bors] - feat(FermatLastTheorem): Add a relaxed variant of FLT allowing nonzero unit solutions #16060

…oprime

github-actions · 2024-08-11T21:51:05Z

PR summary 108762ec7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.NumberTheory.FLT.MasonStothers`	1130

Declarations diff

+ IsCoprime.divRadical
+ IsCoprime.wronskian_eq_zero_iff
+ Polynomial.abc
+ divRadical
+ divRadical_dvd_derivative
+ divRadical_dvd_self
+ divRadical_dvd_wronskian_left
+ divRadical_dvd_wronskian_right
+ divRadical_isUnit
+ divRadical_mul
+ divRadical_ne_zero
+ dvd_derivative_iff
+ eq_divRadical
+ le_max₃_left
+ le_max₃_middle
+ le_max₃_right
+ max₃
+ max₃_add_distrib_right
+ max₃_le
+ max₃_lt
+ max₃_mul_distrib_left
+ mul_radical_divRadical

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.

jcpaik · 2024-08-19T11:07:34Z

Mathlib/NumberTheory/FLT/MasonStothers.lean

+
+
+/-- Auxiliary theorems for `max₃ a b c = max (max a b) c`. -/
+def max₃ (a b c : Nat) : Nat :=


Do we want this auxiliary function for maximum of three natural numbers in the statement of Mason--Stothers? I wonder how other parts of mathlib represent maximum values of three numbers.

We usually just write max (max a b) c, or a ⊔ b ⊔ c if you prefer infixes. But also you are using it to state max (max a b) c ≤ d, in which situation we much prefer writing a ≤ d ∧ b ≤ d ∧ c ≤ d

mathlib4-dependent-issues-bot · 2024-10-26T18:23:08Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid #14873~~
~~[Merged by Bors] - feat(RingTheory/Radical): Theorems for coprime elements + alpha #15331~~
divRadical for polynomials #18452
feat: IsCoprime.wronskian_eq_zero_iff #18483
By Dependent Issues (🤖). Happy coding!

Mathlib/NumberTheory/FLT/MasonStothers.lean

YaelDillies · 2024-10-30T14:27:03Z

Mathlib/NumberTheory/FLT/MasonStothers.lean

+  rwa [divRadical, radical_unit_eq_one hu, EuclideanDomain.div_one]
+
+theorem eq_divRadical {a x : k[X]} (h : (radical a) * x = a) : x = divRadical a := by
+  apply EuclideanDomain.eq_div_of_mul_eq_left (radical_ne_zero a)
+  rwa [mul_comm]
+
+theorem divRadical_hMul {a b : k[X]} (hc : IsCoprime a b) :
+    divRadical (a * b) = (divRadical a) * (divRadical b) := by
+  by_cases ha : a = 0
+  · rw [ha, MulZeroClass.zero_mul, divRadical, EuclideanDomain.zero_div, MulZeroClass.zero_mul]
+  by_cases hb : b = 0
+  · rw [hb, MulZeroClass.mul_zero, divRadical, EuclideanDomain.zero_div, MulZeroClass.mul_zero]
+  symm; apply eq_divRadical
+  rw [radical_mul hc]
+  rw [mul_mul_mul_comm, hMul_radical_divRadical, hMul_radical_divRadical]
+
+theorem divRadical_dvd_self (a : k[X]) : (divRadical a) ∣ a := by
+  rw [divRadical]
+  apply EuclideanDomain.div_dvd_of_dvd
+  exact radical_dvd_self a
+
+/-
+Main lemma: `divRadical a` divides `a'`.
+Proof uses `induction_on_coprime` of `UniqueFactorizationDomain`.
+-/
+theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a) := by
+  induction a using induction_on_coprime
+  · case h0 =>
+    rw [derivative_zero]
+    apply dvd_zero
+  · case h1 a ha =>
+    exact (divRadical_isUnit ha).dvd
+  · case hpr p i hp =>
+    cases i
+    · rw [pow_zero, derivative_one]
+      apply dvd_zero
+    · case succ i =>
+      rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), hMul_radical_divRadical,
+        radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc]
+      apply dvd_mul_of_dvd_left
+      rw [mul_comm, mul_assoc]
+      apply dvd_mul_of_dvd_right
+      rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
+  · -- If it holds for coprime pair a and b, then it also holds for a * b.
+    case hcp x y hpxy hx hy =>
+    have hc : IsCoprime x y :=
+      EuclideanDomain.isCoprime_of_dvd
+        (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
+        fun p hp _ hpx hpy => hp (hpxy hpx hpy)
+    rw [divRadical_hMul hc, derivative_mul]
+    exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)
+
+theorem divRadical_dvd_wronskian_left (a b : k[X]) : (divRadical a) ∣ wronskian a b := by
+  rw [wronskian]
+  apply dvd_sub
+  · apply dvd_mul_of_dvd_left
+    exact divRadical_dvd_self a
+  · apply dvd_mul_of_dvd_left
+    exact divRadical_dvd_derivative a
+
+theorem divRadical_dvd_wronskian_right (a b : k[X]) : (divRadical b) ∣ wronskian a b := by
+  rw [← wronskian_neg_eq, dvd_neg]
+  exact divRadical_dvd_wronskian_left _ _
+
+@[simp]
+theorem dvd_derivative_iff {a : k[X]} : a ∣ derivative a ↔ derivative a = 0 := by
+  constructor
+  · intro h
+    by_cases a_nz : a = 0
+    · rw [a_nz]; simp only [derivative_zero]
+    by_contra deriv_nz
+    have deriv_lt := degree_derivative_lt a_nz
+    have le_deriv := Polynomial.degree_le_of_dvd h deriv_nz
+    have lt_self := le_deriv.trans_lt deriv_lt
+    simp only [lt_self_iff_false] at lt_self
+  intro h; rw [h]; simp
+
+theorem IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) :
+    wronskian a b = 0 ↔ derivative a = 0 ∧ derivative b = 0 := by
+  constructor
+  · intro hw
+    rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw
+    constructor
+    · rw [← dvd_derivative_iff]
+      apply hc.dvd_of_dvd_mul_right
+      rw [← hw]; exact dvd_mul_right _ _
+    · rw [← dvd_derivative_iff]
+      apply hc.symm.dvd_of_dvd_mul_left
+      rw [hw]; exact dvd_mul_left _ _
+  intro hdab
+  cases' hdab with hda hdb
+  rw [wronskian]
+  rw [hda, hdb]; simp only [MulZeroClass.mul_zero, MulZeroClass.zero_mul, sub_self]
+
+
+protected theorem IsCoprime.divRadical {a b : k[X]} (h : IsCoprime a b) :
+    IsCoprime (divRadical a) (divRadical b) := by
+  rw [← hMul_radical_divRadical a] at h
+  rw [← hMul_radical_divRadical b] at h
+  exact h.of_mul_left_right.of_mul_right_right


Could all of this move to a file under Mathlib.RingTheory.Polynomial? Either Mathlib.RingTheory.Polynomial.Wronskian or a new file Mathlib.RingTheory.Polynomial.DivRadical? And can you make that into a separate PR?

I'll put under Mathlib.RingTheory.Polynomial then (IMO these theorems are to specific so I'm not sure if it worths to make new files for it).

I just realized that first half of the theorems & definition of divRadical actually makes sense for EuclideanDomain as well, but not sure if I put these under the "euclidean domain" files. Do you have any suggestions? I think another way is to put divRadical-related theorems, up to divRadical_dvd_self, in Mathlib.RingTheory.Radical with EuclideanDomain version, and put the rest in Mathlib.RingTheory.Polynomial? (Honestly I've never seen any mathematical proofs using $x / \mathrm{rad}(x)$ except for Mason-Stothers...)

I think another way is to put divRadical-related theorems, up to divRadical_dvd_self, in Mathlib.RingTheory.Radical with EuclideanDomain version, and put the rest in Mathlib.RingTheory.Polynomial?

That sounds reasonable, yes

Honestly I've never seen any mathematical proofs using
𝑥
/
𝑟
𝑎
𝑑
(
𝑥
)
except for Mason-Stothers...

You would be surprised how often people have said that their thing had no other application, just before someone else needed it!

For dvd_derivative_iff and IsCoprime.wronskian_eq_zero_iff, I think these are also seperate things. I'd put the second one under Mathlib.RingTheory.Polynomial.Wronskian, but this depends on the first theorem and I don't know where's the best place to put it - do you have any suggestions? (these two are not included in #18452 for now)

No sorry, no suggesyion. I would play around with the code myself but I am momentarily incapactitated by apainful wrist

Mathlib/NumberTheory/FLT/MasonStothers.lean

YaelDillies · 2024-10-30T14:33:53Z

Sorry, I see the review process is dragging along. We really want this in mathlib!

YaelDillies · 2024-10-30T16:56:20Z

Mathlib/NumberTheory/FLT/MasonStothers.lean

      apply abc_subcall wbc <;> assumption
-    constructor
-    · rw [rot3_mul, rot3_mul] at abc_dr_dvd_w ⊢
+    · rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢


Suggested change

· rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢

· rw [← mul_rotate] at abc_dr_dvd_w ⊢

YaelDillies · 2024-10-30T16:56:31Z

Mathlib/NumberTheory/FLT/MasonStothers.lean

-    rw [← divRadical_hMul hab]
-    rw [← divRadical_hMul _]
+    rw [← divRadical_mul hab]
+    rw [← divRadical_mul _]


Suggested change

rw [← divRadical_mul _]

rw [← divRadical_mul]

seewoo5 and others added 19 commits July 18, 2024 09:28

initial commit

e270cb8

remove unnecessary import

b172681

lint

b542624

mathlib.lean

0a9d1af

edit comments

fbb690d

Name changes + edit comments

188206f

Add simp tag

d148c69

theorems for coprime elements

826ce60

address comments

0df94d7

rename alpha -> M

20840c1

minor

c20c796

merge & remove private

5e8f433

remove k

c1da6cd

Merge branch 'feature/element-radical' into feature/element-radical-c…

b7c8561

…oprime

WIP

3a8f6fa

Dig up for Polynomial

15c3196

Uncomment working thms

14b543d

Uncomment all; needs cleanup

74f769a

lint + documentation

878f6a3

seewoo5 assigned jcpaik and seewoo5 Aug 11, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 11, 2024

lint

1425733

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 11, 2024

jcpaik reviewed Aug 19, 2024

View reviewed changes

grunweg changed the title ~~Mason-Stothers theorem (polynomial ABC)~~ feat: Mason-Stothers theorem (polynomial ABC) Aug 22, 2024

grunweg added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Aug 23, 2024

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 26, 2024

leanprover-community deleted a comment from leanprover-community-mathlib4-bot Oct 26, 2024

working version of mason-stothers

35e5896

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 26, 2024

update tactics and fix build errors

258bdc2

YaelDillies reviewed Oct 30, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2024

seewoo5 added 2 commits October 30, 2024 09:36

minor

3bba21e

address more comments

108762e

YaelDillies reviewed Oct 30, 2024

View reviewed changes

seewoo5 mentioned this pull request Oct 30, 2024

feat: dividing an element of a euclidean domain by its radical #18449

Open

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 30, 2024

seewoo5 mentioned this pull request Oct 31, 2024

feat: IsCoprime.wronskian_eq_zero_iff #18483

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Mason-Stothers theorem (polynomial ABC) #15706

feat: Mason-Stothers theorem (polynomial ABC) #15706

seewoo5 commented Aug 11, 2024 •

edited

Loading

github-actions bot commented Aug 11, 2024 •

edited

Loading

Declarations diff

jcpaik Aug 19, 2024 •

edited

Loading

YaelDillies Oct 30, 2024

mathlib4-dependent-issues-bot commented Oct 26, 2024 •

edited

Loading

YaelDillies Oct 30, 2024

seewoo5 Oct 30, 2024

seewoo5 Oct 30, 2024

YaelDillies Oct 30, 2024

YaelDillies Oct 30, 2024

seewoo5 Oct 30, 2024

YaelDillies Oct 30, 2024 •

edited

Loading

YaelDillies commented Oct 30, 2024

YaelDillies Oct 30, 2024

YaelDillies Oct 30, 2024



		/-- Auxiliary theorems for `max₃ a b c = max (max a b) c`. -/
		def max₃ (a b c : Nat) : Nat :=

	· rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢
	· rw [← mul_rotate] at abc_dr_dvd_w ⊢

feat: Mason-Stothers theorem (polynomial ABC) #15706

Are you sure you want to change the base?

feat: Mason-Stothers theorem (polynomial ABC) #15706

Conversation

seewoo5 commented Aug 11, 2024 • edited Loading

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

PR summary 108762ec7a

Import changes for modified files

Declarations diff

jcpaik Aug 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mathlib4-dependent-issues-bot commented Oct 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YaelDillies Oct 30, 2024 • edited Loading

Choose a reason for hiding this comment

YaelDillies commented Oct 30, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

seewoo5 commented Aug 11, 2024 •

edited

Loading

github-actions bot commented Aug 11, 2024 •

edited

Loading

jcpaik Aug 19, 2024 •

edited

Loading

mathlib4-dependent-issues-bot commented Oct 26, 2024 •

edited

Loading

YaelDillies Oct 30, 2024 •

edited

Loading