The monic irreducible closed-form criterion, in characteristic zero or in characteristic larger than the displayed degree bounds. Separability, the differential root extension and constant-residue descent are all constructed from the polynomial and the degree bounds.

Constant residues in characteristic zero or large characteristic. The nonzero annihilating relation and its degree bound are constructed by a Sylvester resultant.

Extend a differential structure to an explicitly separable monic root extension in any characteristic. The construction is the implicit-derivative quotient construction from Mathlib's characteristic-zero instance, with the nonvanishing derivative supplied by separability.

@[reducible]

noncomputable def CCDN.separableAdjoinRootDifferential {K : Type u_1} [Field K] [Differential K] (f : Polynomial K) [Fact (Irreducible f)] [Fact f.Monic] (hsep : f.Separable) : Differential (AdjoinRoot f)

The differential structure on AdjoinRoot f extending the derivation of K, for a monic irreducible separable f: the root α is sent to -(f^D)(α) / f'(α), where f^D is f with its coefficients differentiated.

Equations

• CCDN.separableAdjoinRootDifferential f hsep = { deriv := Derivation.liftOfSurjective ⋯ ⋯ }

theorem CCDN.bivariate_closed_form_eq_gradient {F : Type u_1} [Field F] [IsAlgClosed F] (f g h : Polynomial (Polynomial F)) (hf : Irreducible f) (hm : f.Monic) (hgdeg : g.natDegree < f.natDegree) (hhdeg : h.natDegree < f.natDegree) (D : ℕ) (hfD : ∀ (i : ℕ), (f.coeff i).natDegree ≤ D) (hgD : ∀ (i : ℕ), (g.coeff i).natDegree ≤ D) (hmchar : CharZeroOrGT F f.natDegree) (hchar : CharZeroOrGT F ((f.natDegree + (f.natDegree - 1)) * D)) (hclosed : (bivariateCoefficientDerivative F) g * f - g * (bivariateCoefficientDerivative F) f = Polynomial.derivative h * f - h * Polynomial.derivative f) : ∃ (a : F), g = Polynomial.C (Polynomial.C a) * Polynomial.derivative f ∧ h = Polynomial.C (Polynomial.C a) * (bivariateCoefficientDerivative F) f

Over an algebraically closed field F of characteristic zero or larger than the degree bounds, a monic irreducible bivariate equation has only constant-gradient closed forms within the strict outer-variable degree bounds.