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).

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.