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

refactor(radical,div_radical): Namespace and redundant hypotheses #17

Closed tb65536 closed 1 year ago

tb65536 commented 1 year ago

A couple suggestions. First, if you use namespace polynomial, you can avoid repeatedly writing polynomial.. Second, it's often nice to get rid of a = 0 hypotheses where possible (e.g., by adding an extra case at the start of the lemma), because it can make them easier to use down the road.

seewoo5 commented 1 year ago

Thanks! Looks much clearner.