LeanPool.LeanPolyABC.Corollaries.Davenport #
theorem
LeanPolyABC.ne_zero_of_natDegree_gt_0
{k : Type u_1}
[Field k]
{a : Polynomial k}
(ha : a.natDegree > 0)
:
theorem
LeanPolyABC.Polynomial.davenport
{k : Type u_1}
[Field k]
[CharZero k]
{a b : Polynomial k}
(ha : a.natDegree > 0)
(hb : b.natDegree > 0)
(hnz : a ^ 3 - b ^ 2 ≠ 0)
:
Davenport's theorem
For any nonzero polynomial a, b ∈ k[t] with k of characteristic zero, deg(a) + 2 ≤ 2 * deg(a^3 - b^2).
Proof) Apply ABC for (-a^3, b^2, a^3 - b^2).
theorem
LeanPolyABC.isCoprime_nonzero_c
{k : Type u_1}
[Field k]
{a b : Polynomial k}
(h : IsCoprime a b)
(ha : Polynomial.derivative a ≠ 0)
:
theorem
LeanPolyABC.Polynomial.davenport'
{k : Type u_1}
[Field k]
{a b : Polynomial k}
(hab : IsCoprime a b)
(haderiv : Polynomial.derivative a ≠ 0)
(hbderiv : Polynomial.derivative b ≠ 0)
:
Davenport's theorem for general field k of any characteristic
For any coprime polynomial a, b ∈ k[t] with nonzero derivatives, deg(a) + 2 ≤ 2 * deg(a^3 - b^2). Proof) Apply ABC for (-a^3, b^2, a^3 - b^2).