[Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC)

[seewoo5]

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$.

---

• 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: [Merged by Bors] - feat: divRadical for polynomials #18452
• depends on: [Merged by Bors] - feat: IsCoprime.wronskian_eq_zero_iff #18483

Almost last part of porting project of the formalization of polynomial ABC.

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

Related: #16060

[github-actions]

PR summary 8b3a2a85ac

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.FLT.MasonStothers	1138

---

Declarations diff

+ Polynomial.abc
+ _root_.IsCoprime.wronskian_eq_zero_iff
- IsCoprime.wronskian_eq_zero_iff

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.

[YaelDillies]

maintainer merge

apart from that. Thanks!

[github-actions]

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

[riccardobrasca]

I find the proof easier to read without too many have statement. On the other hand, can you add a little bit of math explanation?

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

[riccardobrasca]

I pushed a small modification to another file. The lines

noncomputable section

open scoped Classical

can now be removed, adding [DecidableEq k]. I suggest a slightly modified proof of the main result:

/-- **Polynomial ABC theorem.** -/
theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
    (hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) :
    ( natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree c + 1 ≤ (radical (a * b * c)).natDegree ) ∨
      derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0 := by
  -- Utility assertions
  have wbc := wronskian_eq_of_sum_zero hsum
  set w := wronskian a b with wab
  have wca : w = wronskian c a := by
    rw [add_rotate] at hsum
    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
  have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
    have adr_dvd_w := divRadical_dvd_wronskian_left a b
    have bdr_dvd_w := divRadical_dvd_wronskian_right a b
    have cdr_dvd_w := divRadical_dvd_wronskian_right b c
    rw [← wab] at adr_dvd_w bdr_dvd_w
    rw [← wbc] at cdr_dvd_w
    rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
    exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
  by_cases hw : w = 0
  · right
    rw [hw] at wab wbc
    cases' hab.wronskian_eq_zero_iff.mp wab.symm with ga gb
    cases' hbc.wronskian_eq_zero_iff.mp wbc.symm with _ gc
    exact ⟨ga, gb, gc⟩
  · left
    refine ⟨?_, ?_, ?_⟩
    · rw [mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wbc <;> assumption
    · rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption
    · apply abc_subcall wab <;> assumption

[jcpaik]

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

I don't get what you mean by this. Are you saying that there is a diamond (I suppose the diamond problem of instance?) in this PR, or some other part of the mathlib that this PR depends on?

[riccardobrasca]

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

I don't get what you mean by this. Are you saying that there is a diamond (I suppose the diamond problem of instance?) in this PR, or some other part of the mathlib that this PR depends on?

It's in another file, but it is fixed by my commit, you can forget about it.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ 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.

[seewoo5]

Thank you all!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build