Porting `Radical.lean` - Githubissues

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 `Radical.lean` #48

Open seewoo5 opened 2 weeks ago

seewoo5 commented 2 weeks ago

[ ] Most of the statements work for UniqueFactorizationMonoid with normalization (or even without normalization, up to unit), so we may upgrade them first by replacing k[X] with general UniqueFactorizationMonoid
[ ] Leave removing normalization condition as a future work
[ ] Put inside RingTheory/UniqueFactorizationDomain.lean? Or make a new lean file Radical.lean somewhere?

Related: UniqueFactorizationMonoid in https://github.com/leanprover-community/mathlib4/blob/dfc07f1b6271219de25170e4936fee9443d4234c/Mathlib/RingTheory/UniqueFactorizationDomain.lean#L192 NormalizationMonoid in https://github.com/leanprover-community/mathlib4/blob/dfc07f1b6271219de25170e4936fee9443d4234c/Mathlib/Algebra/GCDMonoid/Basic.lean#L73