The corner monomial and its remainder
DefinitionEsgk_BivariateCornerNormalFormalgebrapolynomials
This selects the exponent with both coordinates equal to a prescribed integer and subtracts that monomial with its coefficient from a complex bivariate polynomial.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_BidegreeProductRelation
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
namespace Esgk
open MvPolynomial
def bivariateCornerExponent (p : ℕ) : Fin 2 →₀ ℕ :=
Finsupp.single 0 p + Finsupp.single 1 p
def bivariateCornerRemainder (p : ℕ) (Q : BidegreePolynomial ℂ) :
BidegreePolynomial ℂ :=
Q - monomial (bivariateCornerExponent p) (coeff (bivariateCornerExponent p) Q)
end Esgk