seewoo5 / lean-poly-abc

Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4
8 stars 0 forks source link

Non-coprime Mason-Stothers #40

Open jcpaik opened 2 weeks ago

jcpaik commented 2 weeks ago

Copying @seewoo5 from #3

In Stothers' paper, there's a slightly different version of ABC for not necessarily coprime polynomials (Theorem 1.2). Following the proof, it can be translated as follows: for zero-sum distinct triple of nonzero polynomials $a, b, c \in k[t]$, $a + b + c = 0$ implies $\max{\deg(a), \deg(b), \deg(c) } + 1 \le \deg(\mathrm{rad}(a)) + \deg(\mathrm{rad}(b)) + \deg(c)$ (the $\deg(\mathrm{rad}(c))$ of RHS of the original ABC inequality is replaced by $\deg(c)$. Using this, we can remove the coprimality hypothesis for Davenport's theorem (but not sure about the positive characteristic case).

We need to implement this version for completeness.