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

Porting `RationalFunc.lean` #45

Closed jcpaik closed 2 weeks ago

jcpaik commented 2 weeks ago

I don't think a lot of them actually belongs to RatFunc. This is more of a random collection of weird lemmas as of now.