$1/p + 1/q + 1/r \leq 1$ instead of $pq + qr + rp \leq pqr$

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

$1/p + 1/q + 1/r \leq 1$ instead of $pq + qr + rp \leq pqr$ #41

Closed seewoo5 closed 1 month ago

seewoo5 commented 3 months ago

Maybe not important, but we can try to replace hineq: q * r + r * p + p * r \leq p * q * r in flt_catalan with the original form of the assumption 1/p + 1/q + 1/r \leq 1 as in the note.

jcpaik commented 3 months ago

I think people will prefer to work mostly in Nat (no change). But we can ask their opinion on it.