Get rid of `is_coprime.num_denom` once it is merged in mathlib

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 2 weeks ago

jcpaik commented 1 year ago

As this PR in mathlib is merged,

[x] Update mathlib version
[ ] and get rid of is_coprime.num_denom in the proof of elliptic curve parametrization.

jcpaik commented 2 weeks ago

The PR has been merged and we should incorporate this lemma in our code.