The leading homogeneous part along a shear direction

Definition

LeanFormalizations_PachDeZeeuw_CrossingLemma_ShearPartialY

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This defines the univariate polynomial obtained from the top-degree homogeneous part of a plane polynomial by substituting $(X,Y)=(s,1)$ .

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CrossingLemma_Shear
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace PachDeZeeuw.Algebraic

open MvPolynomial


noncomputable def shearTopPoly (h : PlanePoly) : Polynomial ℝ :=
  ∑ m ∈ h.support, (if m 0 + m 1 = h.totalDegree then
    Polynomial.C (coeff m h) * Polynomial.X ^ (m 0) else 0)


end PachDeZeeuw.Algebraic

View graph