degree — Mathlib

English

The degree with respect to a monomial order m is defined by taking the supremum (with respect to the order) of the degrees of monomials appearing in the polynomial.

Русский

Степень по мономильному порядку m определяется как верхняя граница степеней мономов, входящих в данный полином, по этому порядку.

LaTeX

$$$\\deg_m(f) := m.toSyn^{-1}\\big(\\sup_{a \\in \\mathrm{Supp}(f)} m(a)\\big)$$$

Lean4

/-- the degree of a multivariate polynomial with respect to a monomial ordering -/
def degree (f : MvPolynomial σ R) : σ →₀ ℕ :=
  m.toSyn.symm (f.support.sup m.toSyn)

Похожие утверждения