search

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 `Wronskian.lean` #46

Closed jcpaik closed 2 months ago

jcpaik commented 3 months ago

My impression is that a PID scalar ring could be enough.

seewoo5 commented 3 months ago

Wronskian can be defined for "any" ring (maybe commutative, ...) with derivation $D: R \to R$ (see RingTheory/Derivation/Basic.lean), but for now, let's generalize it to polynomial ring but with more general coefficient ring (e.g. CommRing or even SemiRing)

seewoo5 commented 3 months ago

https://github.com/leanprover-community/mathlib4/pull/14243

seewoo5 commented 2 months ago

Related mathlib4 PRs: