search

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

change lt to le #33

Closed seewoo5 closed 1 year ago

seewoo5 commented 1 year ago

This changes the conclusion $X < Y$ of ABC to $X + 1 \leq Y$, which is more often in literature.