Local order of a multivariate polynomial
DefinitionEsgk_MvPolynomialLocalOrderalgebralocal-algebrapolynomials
This defines the local order of a multivariate polynomial by viewing it in the corresponding multivariate power-series ring and taking its power-series order.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
import Mathlib.RingTheory.MvPolynomial.Ideal
import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
namespace MvPolynomial
noncomputable section
variable {R σ : Type*} [CommSemiring R]
def localOrder (p : MvPolynomial σ R) : ℕ∞ :=
MvPowerSeries.order (p : MvPowerSeries σ R)
end
end MvPolynomial