Radial divisibility of homogeneous components

Definition

Esgk_PlaneRadialFiltration

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

algebraic-geometrygeometry

This defines the condition that each degree- $d$ homogeneous component is divisible by $(X^2+Y^2)^{d-m}$ , where the exponent is truncated natural subtraction and is zero for $d\le m$ .

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneRadialQuadratic
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
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 PachDeZeeuw.Algebraic


def IsRadiallyFiltered (m : ℕ) (f : PlanePoly) : Prop :=
  ∀ d, planeRadialQuadratic ^ (d - m) ∣ MvPolynomial.homogeneousComponent d f

namespace IsRadiallyFiltered


end IsRadiallyFiltered


end Esgk

View graph