Mathlib porting plan

[seewoo5]

(Order may change) Always assume that replace our implementation with existing theorems if already exist

1. Preliminaries

• RationalFunc.lean -> FieldTheory/RatFunc/Basic.lean? (Porting RationalFunc.lean #45) -> Migrate to NoParametrization.lean & remove RationalFunc.lean (won't port to mathlib4)
• Wronskian.lean -> Algebra/Polynomial/Wronskian.lean (Porting Wronskian.lean #46)
• Radical.lean -> (Porting Radical.lean #48)
• DivRadical.lean -> (Porting DivRadical.lean #49)
• Max3.lean ->

2. MasonStothers.lean ->

3. Corollaries (make subdirectory in the directory where MasonStothers.lean goes?)

[seewoo5]

I can't find Wronskian in mathlib4, so it seems plausible to do RationalFunc and Wronskian in parallel

[jcpaik]

I'm not sure if the current implementation of Wronskian should be included in mathlib. Wronskian is generally computable for any differentiable function and I was thinking of only adding current Wronskian as a local definition for Mason--Stothers.

...but in retrospective maybe adding Algebra/Polynomial/Wronskian.lean could be also worth doing. It has a lot of good properties (good enough to prove Mason--Stothers).

[seewoo5]

Mathlib FLT https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/FLT/Basic.lean

[seewoo5]

Mason--Stothers leanprover-community/mathlib4#15706
Polynomial FLT leanprover-community/mathlib4#18882