Pain Points

[seewoo5]

• algebraic closure: https://leanprover-community.github.io/mathlib_docs/field_theory/is_alg_closed/algebraic_closure.html#algebraic_closure
• polynomial roots: polynomial.roots, polynomial.root_set
• Maybe we don't need to define actual radical of a polynomial, but only the number of roots.

[seewoo5]

• http://www.fen.bilkent.edu.tr/~franz/ag05/ag-02.pdf
• https://www.isa-afp.org/entries/Mason_Stothers.html already in Isabelle

[seewoo5]

• Defining radical needs to be careful - factors need to be normalized (e.g. only consider monic polynomials). use normalized_factors instead of factors, which is in normalization_monoid
• Prove poly_coprime_disjoint_factors using the definition of is_coprime? -> there are already some related theorems using "gcd"
• gcd_monoid.gcd and euclidean_domain.gcd are different, do not mix up (there are also two versions of gcd_is_unit_iff
• Need nonzero assumption
• You can't use as a.disjoint b for finset a and b, should use disjoint a b (the first is only possible if it was finset.disjoint
• squeeze_simp : more efficient simp (restrict scope)
• n > 0 implies n != 0: just linarith or libsearch (that finds ne_of_gt) or

  intro n0,
  rw n0 at hn,
  simp only [gt_iff_lt, not_lt_zero'] at hn,
  exact hn,

[seewoo5]

• Use dedup instead of multiset.to_finset, then we only need to deal with multiset (no conversions between them), change every related stuff / NO, finset is already multiset! use .val

[seewoo5]

• | and ∣ are different. Latter for the divisibility (use \ + |)

[jcpaik]

with_bot nat is much painful to work with than nat

• We ended up having to prove these lemmas, which are all trivial in nat.

  protected lemma nat.with_bot.add_le_add 
  {a b c d : with_bot ℕ}
  (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := sorry
  -- Note the cursed `smul` multiplication instead of usual multiplication.
  protected lemma nat.with_bot.smul_le_smul 
  {n : ℕ} {a b : with_bot ℕ}
  (h : a ≤ b) : n • a ≤ n • b := sorry

• But then there is a subtlety in working with .nat_degree as well. Zero polynomials are always exceptions.
  • In our proof, the Wronskian is zero so its 'degree' really should be $-\infty$ to work.

    -- not true: counterexample a = b = 1
    lemma wronskian.nat_degree_lt_add {a b : k[X]} 
    (ha : a ≠ 0) (hb : b ≠ 0) : 
    (wronskian a b).nat_degree < a.nat_degree + b.nat_degree := sorry

So, we need to choose one of the painful options.

• Extend the lacking library on with_bot nat to work with .degree
• Painfully go through conversions between .degree and .nat_degree using all the things like with_bot.coe_le_coe, polynomial.degree_eq_nat_degree keeping track of nonzeroness.

[jcpaik]

It's hard to show that the num and denom of a ratfunc are coprime.

Simply trying to rewrite the definition does not work. It results in full gibberish.

theorem is_coprime.num_denom (x : ratfunc k) : is_coprime x.num x.denom :=
begin
  rw [ratfunc.num, ratfunc.denom],
  simp_rw [ratfunc.num_denom],
end

The idea is to mix three things. ratfunc.denom_div and ratfunc.mk_eq_div and ratfunc.induction_on. This is not all all trivial for anyone who is reading this for the first time.

[seewoo5]

The proof of Davenport's theorem by Stothers can be simplified. We don't need to divide into two cases as $\deg(f^3) = \deg(g^2)$ and $\deg(f^3) \neq \deg(g^2)$. Also, some of the earlier assumptions like $f \neq 0, g\neq 0, f^3 - g^2 \neq 0$ actually follows from coprimality and $f' \neq 0 \neq g'$.

[seewoo5]

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

[jcpaik]

@seewoo5 I think we need to work on this slightly different version of ABC for non-coprime polynomials