Improvements on FLT - Githubissues

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

Closed jcpaik closed 1 year ago

jcpaik commented 1 year ago

Lesser is_coprime options in FLT
Two versions of FLT: one with is_coprime precondition and any field char, and another with no is_coprime precondition and char zero.

seewoo5 commented 1 year ago

Why do we need two?