Porting `DivRadical.lean`

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

Open seewoo5 opened 3 months ago

seewoo5 commented 3 months ago

After #48

[ ] This is definitely something on polynomials. Put in Algebra/Polynomial/Div.lean?
[x] More general ring? -> Maybe not, the most important theorem we need is $a / \mathrm{rad}(a) | a'$ for polynomials, and it is not essential to define divRadical for the purpose.