Mathlib-Facing Bivariate Multiplicity Helpers

This file collects multiplicity- and discriminant-oriented helpers for Mathlib's bivariate polynomial surface R[X][Y].

noncomputable def Polynomial.Bivariate.rootMultiplicity₀ {F : Type u_1} [Semiring F] [DecidableEq F] (f : Polynomial (Polynomial F)) : Option ℕ

Root multiplicity of a bivariate polynomial at the origin.

noncomputable def Polynomial.Bivariate.shift {F : Type u_1} [CommSemiring F] (f : Polynomial (Polynomial F)) (x y : F) : Polynomial (Polynomial F)

Shift a bivariate polynomial by (x, y).

noncomputable def Polynomial.Bivariate.rootMultiplicity {F : Type u_1} [CommSemiring F] [DecidableEq F] (f : Polynomial (Polynomial F)) (x y : F) : Option ℕ

Root multiplicity (order of vanishing) of a bivariate polynomial at (x, y).

theorem Polynomial.Bivariate.rootMultiplicity₀_ge_iff {F : Type u_1} [CommSemiring F] [DecidableEq F] (g : Polynomial (Polynomial F)) (r : ℕ) : (∀ (i j : ℕ), i + j < r → coeff g i j = 0) ↔ ∀ m ∈ rootMultiplicity₀ g, r ≤ m

rootMultiplicity₀ g is at least r (vacuously so when g = 0, where it is none) iff every coefficient of total degree < r vanishes.

noncomputable def Polynomial.Bivariate.discr_y {F : Type u_1} [CommRing F] (f : Polynomial (Polynomial F)) : Polynomial F

A discriminant-like helper in the outer Y variable.

Unlike Mathlib's univariate discr, this returns 0 for constant bivariate polynomials.